A,B:Type, f:(A onto B), a:. a onto A  (B Discrete)  Surj(A; B; f)

By:	Auto THEN Rename-2: s THEN Use:[a | A | B | f | s] Inst: Thm*  f:(B onto C), g:(A onto B). f o g  A onto C THEN FwdThru:  Thm*  (A Discrete)  (e:(AA). x,y:A. (x e y)  x = y) on [ B Discrete ] THEN Analyze-1

1

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)

10 steps

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