Nuprl - Proof: nsub bij ooc invpair 1 2 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: nsub bij ooc invpair 1 2 1

1. a :

2. (

f.<f,

y.least x:

. f(x)=

y>)

(

a bij

a
3. f :

a
4. g :

a
5. InvFuns(

a;f;g)

Bij(

a; f)

By:	FwdThru: Thm* InvFuns(A;B;f;g) Bij(A; B; f) on [ InvFuns(a;a;f;g) ]

Generated subgoals:

None

About:

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