PrintForm Definitions finite sets Sections AutomataTheory Doc

At: one one preser fin 1 1 1 1 1 1 1 1 1 1
1. T: Type
2. S: Type
3. n:
4. f: nT
5. Bij(n; T; f)
6. f1: TS
7. g: ST
8. g o f1 = Id
9. f1 o g = Id
10. a1: n
11. a2: n
12. (f1 o f)(a1) = (f1 o f)(a2)
13. (g o f1 o f)(a1) = (g o f1 o f)(a2)

a1 = a2
By: RWH (LemmaC Thm* f:(AB), g:(BC), h:(CD). h o (g o f) = (h o g) o f AD) 13
Generated subgoal:

113. (g o f1 o f)(a1) = (g o f1 o f)(a2)
a1 = a2

About:
equalnatural_numberuniversefunctionapply