PrintForm Definitions exponent Sections AutomataTheory Doc

At: fun preserves fin 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 2 1 1 1
1. S: Type
2. T: Type
3. n:
4. f: nS
5. g: Sn
6. g o f = Id & f o g = Id
7. n1:
8. f1: n1T
9. g1: Tn1
10. g1 o f1 = Id
11. f1 o g1 = Id
12. f2: (nn1)(n1n)
13. g2: (n1n)nn1
14. g2 o f2 = Id
15. f2 o g2 = Id
16. x: ST

f1 o g2(f2(g1 o x o f)) o g = x
By: RWH (LemmaC Thm* f:(AB), g:(BC), h:(CD). h o (g o f) = (h o g) o f AD) 0
Generated subgoal:

1 f1 o g2(f2(g1 o x o f)) o g = x

About:
equalfunctionapplyuniversenatural_numberand