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 5;
then ( dom (uncurry f) c= [:(dom f),Y:] & dom (uncurry' f) c= [:Y,(dom f):] & [:(dom f),Y:] c= [:X,Y:] & [:Y,(dom f):] c= [:Y,X:] ) by FUNCT_5:44, ZFMISC_1:119;
then ( rng (uncurry f) c= Z & rng (uncurry' f) c= Z & dom (uncurry f) c= [:X,Y:] & dom (uncurry' f) c= [:Y,X:] ) by A1, FUNCT_5:47, XBOOLE_1:1;
hence ( uncurry f in PFuncs [:X,Y:],Z & uncurry' f in PFuncs [:Y,X:],Z ) by PARTFUN1:def 5; :: thesis: verum