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 Th15;
assume dom f c= [:V1,V2:] ; :: thesis: f in PFuncs ([:X,Y:],Z)
hence f in PFuncs ([:X,Y:],Z) by A1, FUNCT_5:50; :: thesis: verum