let X, Y, Z be set ; :: thesis: for f being Function st f in PFuncs (X,(PFuncs (Y,Z))) holds
( uncurry f in PFuncs ([:X,Y:],Z) & uncurry' f in PFuncs ([:Y,X:],Z) )
let f be Function; :: thesis: ( f in PFuncs (X,(PFuncs (Y,Z))) implies ( uncurry f in PFuncs ([:X,Y:],Z) & uncurry' f in PFuncs ([:Y,X:],Z) ) )
assume f in PFuncs (X,(PFuncs (Y,Z))) ; :: thesis: ( uncurry f in PFuncs ([:X,Y:],Z) & uncurry' f in PFuncs ([:Y,X:],Z) )
then A1: ex g being Function st
( f = g & dom g c= X & rng g c= PFuncs (Y,Z) ) by PARTFUN1:def 3;
then ( dom (uncurry f) c= [:(dom f),Y:] & [:(dom f),Y:] c= [:X,Y:] ) by FUNCT_5:37, ZFMISC_1:96;
then A2: dom (uncurry f) c= [:X,Y:] ;
( dom (uncurry' f) c= [:Y,(dom f):] & [:Y,(dom f):] c= [:Y,X:] ) by A1, FUNCT_5:37, ZFMISC_1:96;
then A3: dom (uncurry' f) c= [:Y,X:] ;
( rng (uncurry f) c= Z & rng (uncurry' f) c= Z ) by A1, FUNCT_5:40;
hence ( uncurry f in PFuncs ([:X,Y:],Z) & uncurry' f in PFuncs ([:Y,X:],Z) ) by A2, A3, PARTFUN1:def 3; :: thesis: verum