PrintForm Definitions finite sets Sections AutomataTheory Doc

At: one2one preserves fin 1 1 1
1. T: Type
2. U: Type
3. f: TU
4. g:(UT). InvFuns(T; U; f; g)
5. Fin(T)

Fin(U)
By: Analyze 4
Generated subgoal:

14. g: UT
5. InvFuns(T; U; f; g)
6. Fin(T)
Fin(U)

About:
universefunctionexists