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 A1: ( ( 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 ) ; :: thesis: f in PFuncs X,(PFuncs Y,Z)
then A2: ( 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 PARTFUN1:def 5;
then ( uncurry' f = ~ (uncurry f) & ( ( dom (uncurry f) c= [:X,Y:] & rng (uncurry f) c= Z ) or ( dom (uncurry' f) c= [:Y,X:] & rng (uncurry' f) c= Z ) ) ) by FUNCT_5:def 6;
then A3: dom (uncurry' f) c= [:Y,X:] by 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 A4: y in rng f ; :: thesis: y in PFuncs Y,Z
then ex g being Function st
( y = g & dom g c= V1 & rng g c= V2 ) by A1, PARTFUN1:def 5;
then reconsider h = y as Function ;
consider x being set such that
A5: ( x in dom f & y = f . x ) by A4, FUNCT_1:def 5;
A6: 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 A5, FUNCT_5:46;
hence z in Y by A3, ZFMISC_1:106; :: thesis: verum

end;

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 A5, FUNCT_5:45, FUNCT_5:46;
hence z in Z by A2; :: thesis: verum

end;

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

end;

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