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 that
A1: ( uncurry f in Funcs ([:X,Y:],Z) or uncurry' f in Funcs ([:Y,X:],Z) ) and
A2: rng f c= PFuncs (V1,V2) and
A3: dom f = X ; :: thesis: f in Funcs (X,(Funcs (Y,Z)))
A4: uncurry' f = ~ (uncurry f) by FUNCT_5:def 4;
A5: ( 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 A1, FUNCT_2:def 2;
then A6: dom (uncurry' f) = [:Y,X:] by A4, FUNCT_4:46;
rng f c= Funcs (Y,Z)

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng f or y in Funcs (Y,Z) )
assume A7: y in rng f ; :: thesis: y in Funcs (Y,Z)
then consider x being object such that
A8: x in dom f and
A9: 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, A7, PARTFUN1:def 3;
then reconsider h = y as Function ;
A10: dom h = Y

proof

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

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 A8, A9, FUNCT_5:39;
hence z in Y by A6, ZFMISC_1:87; :: thesis: verum

end;

let z be object ; :: 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 A3, A8, ZFMISC_1:87;
then [x,z] in dom (uncurry f) by A4, A6, FUNCT_4:42;
then consider y1 being object , f1 being Function, y2 being object such that
A11: [x,z] = [y1,y2] and
y1 in dom f and
A12: ( f1 = f . y1 & y2 in dom f1 ) by FUNCT_5:def 2;
x = y1 by A11, XTUPLE_0:1;
hence z in dom h by A9, A11, A12, XTUPLE_0:1; :: thesis: verum

end;

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 A8, A9, FUNCT_5:38, FUNCT_5:39;
hence z in Z by A5; :: thesis: verum

end;

hence y in Funcs (Y,Z) by A10, FUNCT_2:def 2; :: thesis: verum

end;

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