let X, Y, Z, V1, V2 be set ; :: thesis: 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)))
let f be Function; :: thesis: ( ( 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 implies f in PFuncs (X,(PFuncs (Y,Z))) )
assume that
A1: ( uncurry f in PFuncs ([:X,Y:],Z) or uncurry' f in PFuncs ([:Y,X:],Z) ) and
A2: rng f c= PFuncs (V1,V2) and
A3: dom f c= X ; :: thesis: f in PFuncs (X,(PFuncs (Y,Z)))
A4: ( ex g being Function st
( uncurry f = g & dom g c= [:X,Y:] & rng g c= Z ) or ex g being Function st
( uncurry' f = g & dom g c= [:Y,X:] & rng g c= Z ) ) by A1, PARTFUN1:def 3;
uncurry' f = ~ (uncurry f) by FUNCT_5:def 4;
then A5: dom (uncurry' f) c= [:Y,X:] by A4, FUNCT_4:45;
rng f c= PFuncs (Y,Z)

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng f or y in PFuncs (Y,Z) )
assume A6: y in rng f ; :: thesis: y in PFuncs (Y,Z)
then consider x being object such that
A7: ( x in dom f & y = f . x ) by FUNCT_1:def 3;
ex g being Function st
( y = g & dom g c= V1 & rng g c= V2 ) by A2, A6, PARTFUN1:def 3;
then reconsider h = y as Function ;
A8: rng h c= Z

proof

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in rng h or z in Z )
assume z in rng h ; :: thesis: z in Z
then ex y1 being object st
( y1 in dom h & z = h . y1 ) by FUNCT_1:def 3;
then ( z in rng (uncurry f) & z in rng (uncurry' f) ) by A7, FUNCT_5:38, FUNCT_5:39;
hence z in Z by A4; :: thesis: verum

end;

dom h c= Y

proof

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in dom h or z in Y )
assume z in dom h ; :: thesis: z in Y
then [z,x] in dom (uncurry' f) by A7, FUNCT_5:39;
hence z in Y by A5, ZFMISC_1:87; :: thesis: verum

end;

hence y in PFuncs (Y,Z) by A8, PARTFUN1:def 3; :: thesis: verum

end;

hence f in PFuncs (X,(PFuncs (Y,Z))) by A3, PARTFUN1:def 3; :: thesis: verum