let X, Y, Z, D be set ; :: thesis: ( D c= Funcs X,(Funcs Y,Z) implies ex F being ManySortedSet of D st
( F is uncurrying & rng F c= Funcs [:X,Y:],Z ) )
assume A1: D c= Funcs X,(Funcs Y,Z) ; :: thesis: ex F being ManySortedSet of D st
( F is uncurrying & rng F c= Funcs [:X,Y:],Z )

per cases ( D is empty or not D is empty ) ;

suppose D is empty ; :: thesis: ex F being ManySortedSet of D st
( F is uncurrying & rng F c= Funcs [:X,Y:],Z )

then reconsider F = {} as ManySortedSet of D by PARTFUN1:def 4, RELAT_1:60, RELAT_1:def 18;
take F ; :: thesis: ( F is uncurrying & rng F c= Funcs [:X,Y:],Z )
thus F is uncurrying ; :: thesis: rng F c= Funcs [:X,Y:],Z
thus rng F c= Funcs [:X,Y:],Z by RELAT_1:60, XBOOLE_1:2; :: thesis: verum

end;

suppose not D is empty ; :: thesis: ex F being ManySortedSet of D st
( F is uncurrying & rng F c= Funcs [:X,Y:],Z )

then reconsider E = D as non empty functional set by A1;
deffunc H₁( Function) -> set = uncurry $1;
consider F being ManySortedSet of E such that
A2: for d being Element of E holds F . d = H₁(d) from PBOOLE:sch 5();
reconsider F1 = F as ManySortedSet of D ;
take F1 ; :: thesis: ( F1 is uncurrying & rng F1 c= Funcs [:X,Y:],Z )
thus F1 is uncurrying :: thesis: rng F1 c= Funcs [:X,Y:],Z

proof

hereby :: according to WAYBEL27:def 1 :: thesis: for f being Function st f in dom F1 holds
F1 . f = uncurry f

let x be set ; :: thesis: ( x in dom F1 implies x is Function-yielding Function )
assume x in dom F1 ; :: thesis: x is Function-yielding Function
then x in D by PARTFUN1:def 4;
then consider x1 being Function such that
A3: x1 = x and
dom x1 = X and
A4: rng x1 c= Funcs Y,Z by A1, FUNCT_2:def 2;
x1 is Function-yielding

proof

let a be set ; :: according to FUNCOP_1:def 6 :: thesis: ( not a in proj1 x1 or x1 . a is set )
assume a in dom x1 ; :: thesis: x1 . a is set
then x1 . a in rng x1 by FUNCT_1:def 5;
hence x1 . a is set by A4; :: thesis: verum

end;

hence x is Function-yielding Function by A3; :: thesis: verum

end;

let f be Function; :: thesis: ( f in dom F1 implies F1 . f = uncurry f )
assume f in dom F1 ; :: thesis: F1 . f = uncurry f
then reconsider d = f as Element of E by PARTFUN1:def 4;
thus F1 . f = F . d
.= uncurry f by A2 ; :: thesis: verum

end;

thus rng F1 c= Funcs [:X,Y:],Z :: thesis: verum

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng F1 or y in Funcs [:X,Y:],Z )
assume y in rng F1 ; :: thesis: y in Funcs [:X,Y:],Z
then consider x being set such that
A5: x in dom F1 and
A6: y = F1 . x by FUNCT_1:def 5;
reconsider d = x as Element of E by A5, PARTFUN1:def 4;
A7: d in Funcs X,(Funcs Y,Z) by A1, TARSKI:def 3;
y = uncurry d by A2, A6;
hence y in Funcs [:X,Y:],Z by A7, FUNCT_6:20; :: thesis: verum

end;

end;

end;