Nuprl - Proof: nsub bij ooc invpair 1 3 2 1 1 1

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

1. a :

2. (

f.<f,

y.least x:

. f(x)=

y>)

(

a bij

a
3. (

fg.fg/f,g. f)

(

a bij

a
4. f :

a
5. g :

a
6. InvFuns(

a;f;g)

a onto

By:

Analyze

Generated subgoal:

1 Surj(a; a; f)
1 step

About:

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