let X, Y, Z, V1, V2 be set ; :: thesis: for f being Function st ( uncurry f in Funcs [:X,Y:],Z or uncurry' f in Funcs [:Y,X:],Z ) & rng f c= PFuncs V1,V2 & dom f = X holds
f in Funcs X,(Funcs Y,Z)
let f be Function; :: thesis: ( ( uncurry f in Funcs [:X,Y:],Z or uncurry' f in Funcs [:Y,X:],Z ) & rng f c= PFuncs V1,V2 & dom f = X implies f in Funcs X,(Funcs Y,Z) )
assume A1: ( ( uncurry f in Funcs [:X,Y:],Z or uncurry' f in Funcs [:Y,X:],Z ) & rng f c= PFuncs V1,V2 & dom f = X ) ; :: thesis: f in Funcs X,(Funcs Y,Z)
then A2: ( ex g being Function st
( uncurry f = g & dom g = [:X,Y:] & rng g c= Z ) or ex g being Function st
( uncurry' f = g & dom g = [:Y,X:] & rng g c= Z ) ) by FUNCT_2:def 2;
then A3: ( uncurry' f = ~ (uncurry f) & ( ( dom (uncurry f) = [:X,Y:] & rng (uncurry f) c= Z ) or ( dom (uncurry' f) = [:Y,X:] & rng (uncurry' f) c= Z ) ) ) by FUNCT_5:def 6;
then A4: dom (uncurry' f) = [:Y,X:] by FUNCT_4:47;
rng f c= Funcs Y,Z

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng f or y in Funcs Y,Z )
assume A5: y in rng f ; :: thesis: y in Funcs 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
A6: ( x in dom f & y = f . x ) by A5, FUNCT_1:def 5;
A7: dom h = Y

proof

thus dom h c= Y :: according to XBOOLE_0:def 10 :: thesis: Y c= dom h

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 A6, FUNCT_5:46;
hence z in Y by A4, ZFMISC_1:106; :: thesis: verum

end;

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in Y or z in dom h )
assume z in Y ; :: thesis: z in dom h
then [z,x] in [:Y,X:] by A1, A6, ZFMISC_1:106;
then [x,z] in dom (uncurry f) by A3, A4, FUNCT_4:43;
then consider y1 being set , f1 being Function, y2 being set such that
A8: ( [x,z] = [y1,y2] & y1 in dom f & f1 = f . y1 & y2 in dom f1 ) by FUNCT_5:def 4;
( x = y1 & z = y2 ) by A8, ZFMISC_1:33;
hence z in dom h by A6, A8; :: 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 A6, FUNCT_5:45, FUNCT_5:46;
hence z in Z by A2; :: thesis: verum

end;

hence y in Funcs Y,Z by A7, FUNCT_2:def 2; :: thesis: verum

end;

hence f in Funcs X,(Funcs Y,Z) by A1, FUNCT_2:def 2; :: thesis: verum