Level: Lib Thy Top: 1
Hypotheses:

  1. T :

  2. S :

  3. (n:. f:n T. Bij(n;T;f)) (f:T S. g:S T. InvFuns(T;S;f;g))

Conclusion:

n:. f:n S. Bij(n;S;f)

Applied Tactic: D 3 THEN D 3 THEN D 4
Generated subgoals:

1. n:. f:n S. Bij(n;S;f)