PrintForm Definitions automata 5 Sections AutomataTheory Doc

At: surj is inj gen 1 1 1 1 2 1 1 1 1 1 1 1
1. A: Type
2. B: Type
3. f: AB
4. f1: AB
5. g: BA
6. InvFuns(A; B; f1; g)
7. n:
8. f2: nB
9. g1: Bn
10. InvFuns(n; B; f2; g1)
11. Surj(A; B; f)
12. a1: A
13. a2: A
14. f(a1) = f(a2)

(g1 o f o g o f2 o g1)(f1(a1)) = (g1 o f o g o f2 o g1)(f1(a2))
By:
RW (AddrC [2;1;2] (RevLemmaC Thm* f:(AB), g:(BC), h:(CD). h o (g o f) = (h o g) o f AD)) 0
THEN
RW (AddrC [3;1;2] (RevLemmaC Thm* f:(AB), g:(BC), h:(CD). h o (g o f) = (h o g) o f AD)) 0
Generated subgoal:

1 (g1 o f o g o f2 o g1)(f1(a1)) = (g1 o f o g o f2 o g1)(f1(a2))

About:
equalnatural_numberapplyuniversefunction