let X, Y, Z, V1, V2 be set ; :: thesis: for f being Function st ( curry f in PFuncs X,(PFuncs Y,Z) or curry' f in PFuncs Y,(PFuncs X,Z) ) & dom f c= [:V1,V2:] holds
f in PFuncs [:X,Y:],Z
let f be Function; :: thesis: ( ( curry f in PFuncs X,(PFuncs Y,Z) or curry' f in PFuncs Y,(PFuncs X,Z) ) & dom f c= [:V1,V2:] implies f in PFuncs [:X,Y:],Z )
assume ( curry f in PFuncs X,(PFuncs Y,Z) or curry' f in PFuncs Y,(PFuncs X,Z) ) ; :: thesis: ( not dom f c= [:V1,V2:] or f in PFuncs [:X,Y:],Z )
then A1: ( uncurry (curry f) in PFuncs [:X,Y:],Z or uncurry' (curry' f) in PFuncs [:X,Y:],Z ) by Th24;
assume dom f c= [:V1,V2:] ; :: thesis: f in PFuncs [:X,Y:],Z
hence f in PFuncs [:X,Y:],Z by A1, FUNCT_5:57; :: thesis: verum