Level: Lib Thy Top: 1 1
Hypotheses:

  1. T :

  2. U :

  3. 1-1-Corresp(T;U)

  4. Fin(T)

Conclusion:

Fin(U)

Applied Tactic: D 3
Generated subgoals:

1. Fin(U)