PrintForm Definitions finite sets Sections AutomataTheory Doc

At: one2one preserves fin 1 1 1 1 1
1. T: Type
2. U: Type
3. f: TU
4. g: UT
5. g o f = Id
6. f o g = Id
7. Fin(T)

Fin(U)
By: Analyze 7
Generated subgoal:

17. n:
8. f:(nT). Bij(n; T; f)
Fin(U)

About:
universefunctionequal