theorem :: FUNCT_6:17

for X, Y, Z, V1, V2 being set
for f being Function st ( uncurry f in PFuncs ([:X,Y:],Z) or uncurry' f in PFuncs ([:Y,X:],Z) ) & rng f c= PFuncs (V1,V2) & dom f c= X holds
f in PFuncs (X,(PFuncs (Y,Z)))