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