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 5;
uncurry' f = ~ (uncurry f) by FUNCT_5:def 6;
then A5: dom (uncurry' f) c= [:Y,X:] by A4, FUNCT_4:46;
rng f c= PFuncs Y,Z

proof

let y be set ; :: 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 set such that
A7: ( x in dom f & y = f . x ) by FUNCT_1:def 5;
ex g being Function st
( y = g & dom g c= V1 & rng g c= V2 ) by A2, A6, PARTFUN1:def 5;
then reconsider h = y as Function ;
A8: rng h c= Z

proof

let z be set ; :: 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 set st
( y1 in dom h & z = h . y1 ) by FUNCT_1:def 5;
then ( z in rng (uncurry f) & z in rng (uncurry' f) ) by A7, FUNCT_5:45, FUNCT_5:46;
hence z in Z by A4; :: thesis: verum

end;

dom h c= Y

proof

let z be set ; :: 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:46;
hence z in Y by A5, ZFMISC_1:106; :: thesis: verum

end;

hence y in PFuncs Y,Z by A8, PARTFUN1:def 5; :: thesis: verum

end;

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