At: surj is inj gen111111111111111111 1. A: Type 2. B: Type 3. f: AB 4. f1: AB 5. g: BA 6. g o f1 = Id 7. f1 o g = Id 8. n: 9. f2: nB 10. g1: Bn 11. g1 o f2 = Id 12. f2 o g1 = Id 13. b: n 14. a: A 15. f(a) = f2(b)
g1(f(a)) = b By: ApFunToHypEquands `z' (g1(z)) n 15 Generated subgoal:
g1(f(a)) = b
B
