Nuprl - Proof: nsub surj ooc nsub bij

IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: nsub surj ooc nsub bij

. (

k onto

k) ~ (

k bij

By:	Auto THEN OOCifExteq THEN BackThru: Thm* (k onto k) =ext (k bij k)

Generated subgoals:

None

About:

IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html