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