1. A : Type
2. B : Type
3. f : A onto B
4. a : 
5. s : a onto A
6. B Discrete
7. f o s  a onto B
8. e : BB
9. x,y:B. (x e y)  x = y
  Surj(A; B; f)

By:	Analyze5 THEN Analyze3 THEN Analyze-3 THEN (9) Def of <term>  <type>

1

3. f : AB 4. Surj(A; B; f)  [not for witness] 5. a :  6. s : aA 7. Surj(a; A; s)  [not for witness] 8. B Discrete 9. f o s  aB 10. Surj(a; B; f o s)  [not for witness] 11. e : BB 12. x,y:B. (x e y)  x = y   Surj(A; B; f)

9 steps

About: IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html