let X, Y, Z be set ; :: thesis: for f being Function st f in PFuncs ([:X,Y:],Z) holds
( curry f in PFuncs (X,(PFuncs (Y,Z))) & curry' f in PFuncs (Y,(PFuncs (X,Z))) )
let f be Function; :: thesis: ( f in PFuncs ([:X,Y:],Z) implies ( curry f in PFuncs (X,(PFuncs (Y,Z))) & curry' f in PFuncs (Y,(PFuncs (X,Z))) ) )
assume f in PFuncs ([:X,Y:],Z) ; :: thesis: ( curry f in PFuncs (X,(PFuncs (Y,Z))) & curry' f in PFuncs (Y,(PFuncs (X,Z))) )
then A1: ex g being Function st
( f = g & dom g c= [:X,Y:] & rng g c= Z ) by PARTFUN1:def 3;
then ( proj1 [:X,Y:] c= X & proj1 (dom f) c= proj1 [:X,Y:] ) by FUNCT_5:10, XTUPLE_0:8;
then proj1 (dom f) c= X ;
then A2: PFuncs ((proj1 (dom f)),(rng f)) c= PFuncs (X,Z) by A1, PARTFUN1:50;
( proj2 [:X,Y:] c= Y & proj2 (dom f) c= proj2 [:X,Y:] ) by A1, FUNCT_5:10, XTUPLE_0:9;
then proj2 (dom f) c= Y ;
then ( rng (curry f) c= PFuncs ((proj2 (dom f)),(rng f)) & PFuncs ((proj2 (dom f)),(rng f)) c= PFuncs (Y,Z) ) by A1, FUNCT_5:36, PARTFUN1:50;
then A3: rng (curry f) c= PFuncs (Y,Z) ;
rng (curry' f) c= PFuncs ((proj1 (dom f)),(rng f)) by FUNCT_5:36;
then A4: rng (curry' f) c= PFuncs (X,Z) by A2;
( dom (curry f) c= X & dom (curry' f) c= Y ) by A1, FUNCT_5:25;
hence ( curry f in PFuncs (X,(PFuncs (Y,Z))) & curry' f in PFuncs (Y,(PFuncs (X,Z))) ) by A3, A4, PARTFUN1:def 3; :: thesis: verum