let X, Y, Z, D be set ; :: thesis: ( D c= Funcs ([:X,Y:],Z) implies ex F being ManySortedSet of D st
( F is currying & ( ( Y = {} implies X = {} ) implies rng F c= Funcs (X,(Funcs (Y,Z))) ) ) )
assume A1: D c= Funcs ([:X,Y:],Z) ; :: thesis: ex F being ManySortedSet of D st
( F is currying & ( ( Y = {} implies X = {} ) implies rng F c= Funcs (X,(Funcs (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 currying & ( ( Y = {} implies X = {} ) implies rng F c= Funcs (X,(Funcs (Y,Z))) ) )

then reconsider F = {} as ManySortedSet of D by PARTFUN1:def 2, RELAT_1:38, RELAT_1:def 18;
take F ; :: thesis: ( F is currying & ( ( Y = {} implies X = {} ) implies rng F c= Funcs (X,(Funcs (Y,Z))) ) )
thus F is currying ; :: thesis: ( ( Y = {} implies X = {} ) implies rng F c= Funcs (X,(Funcs (Y,Z))) )
assume ( Y = {} implies X = {} ) ; :: thesis: rng F c= Funcs (X,(Funcs (Y,Z)))
thus rng F c= Funcs (X,(Funcs (Y,Z))) ; :: thesis: verum

end;

suppose not D is empty ; :: thesis: ex F being ManySortedSet of D st
( F is currying & ( ( Y = {} implies X = {} ) implies rng F c= Funcs (X,(Funcs (Y,Z))) ) )

then reconsider E = D as non empty functional set by A1;
deffunc H₁( Function) -> set = curry $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 currying & ( ( Y = {} implies X = {} ) implies rng F1 c= Funcs (X,(Funcs (Y,Z))) ) )
thus F1 is currying :: thesis: ( ( Y = {} implies X = {} ) implies rng F1 c= Funcs (X,(Funcs (Y,Z))) )

proof

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

let x be set ; :: thesis: ( x in dom F1 implies ( x is Function & proj1 x is Relation ) )
assume x in dom F1 ; :: thesis: ( x is Function & proj1 x is Relation )
then A3: x in D ;
hence x is Function by A1; :: thesis: proj1 x is Relation
ex x1 being Function st
( x1 = x & dom x1 = [:X,Y:] & rng x1 c= Z ) by A3, A1, FUNCT_2:def 2;
hence proj1 x is Relation ; :: thesis: verum

end;

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

end;

assume A4: ( Y = {} implies X = {} ) ; :: thesis: rng F1 c= Funcs (X,(Funcs (Y,Z)))
thus rng F1 c= Funcs (X,(Funcs (Y,Z))) :: thesis: verum

proof

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

per cases ( [:X,Y:] = {} or [:X,Y:] <> {} ) ;

suppose A9: [:X,Y:] = {} ; :: thesis: y in Funcs (X,(Funcs (Y,Z)))

then A10: d is Function of {},Z by A8, FUNCT_2:66;

now :: thesis: ( X = {} implies y in Funcs (X,(Funcs (Y,Z))) )

assume A11: X = {} ; :: thesis: y in Funcs (X,(Funcs (Y,Z)))
then y is Function of X,(Funcs (Y,Z)) by A7, A10, FUNCT_5:42, RELSET_1:12;
hence y in Funcs (X,(Funcs (Y,Z))) by A11, FUNCT_2:8; :: thesis: verum

end;

hence y in Funcs (X,(Funcs (Y,Z))) by A4, A9; :: thesis: verum

end;

suppose [:X,Y:] <> {} ; :: thesis: y in Funcs (X,(Funcs (Y,Z)))

hence y in Funcs (X,(Funcs (Y,Z))) by A7, A8, FUNCT_6:10; :: thesis: verum

end;

end;

end;

end;

end;