Nuprl - Proof: nsub bij ooc invpair 1 3 2 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. 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)

(

f.<f,

y.least x:

. f(x)=

y>)((

fg.fg/f,g. f)(<f,g>)) = <f,g>

By:	Reduce Concl

Generated subgoal:

1 <f,y.least x:. f(x)=y> = <f,g> aa
12 steps

About:

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