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 5;
then ( proj1 [:X,Y:] c= X & proj1 (dom f) c= proj1 [:X,Y:] ) by FUNCT_5:5, FUNCT_5:12;
then proj1 (dom f) c= X by XBOOLE_1:1;
then A2: PFuncs ((proj1 (dom f)),(rng f)) c= PFuncs (X,Z) by A1, PARTFUN1:128;
( proj2 [:X,Y:] c= Y & proj2 (dom f) c= proj2 [:X,Y:] ) by A1, FUNCT_5:5, FUNCT_5:12;
then proj2 (dom f) c= Y by XBOOLE_1:1;
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:43, PARTFUN1:128;
then A3: rng (curry f) c= PFuncs (Y,Z) by XBOOLE_1:1;
rng (curry' f) c= PFuncs ((proj1 (dom f)),(rng f)) by FUNCT_5:43;
then A4: rng (curry' f) c= PFuncs (X,Z) by A2, XBOOLE_1:1;
( dom (curry f) c= X & dom (curry' f) c= Y ) by A1, FUNCT_5:32;
hence ( curry f in PFuncs (X,(PFuncs (Y,Z))) & curry' f in PFuncs (Y,(PFuncs (X,Z))) ) by A3, A4, PARTFUN1:def 5; :: thesis: verum