let C, D, E be non empty set ; :: thesis: for f being Function of [:C,D:],E holds curry f is Function of C,(Funcs (D,E))
let f be Function of [:C,D:],E; :: thesis: curry f is Function of C,(Funcs (D,E))
A1: dom f = [:C,D:] by FUNCT_2:def 1;
A2: rng (curry f) c= Funcs (D,E)

proof

A3: rng (curry f) c= Funcs (D,(rng f)) by A1, Th28;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng (curry f) or x in Funcs (D,E) )
assume x in rng (curry f) ; :: thesis: x in Funcs (D,E)
then consider g being Function such that
A4: x = g and
A5: dom g = D and
A6: rng g c= rng f by A3, FUNCT_2:def 2;
rng g c= E by A6, XBOOLE_1:1;
then g is Function of D,E by A5, FUNCT_2:def 1, RELSET_1:4;
hence x in Funcs (D,E) by A4, FUNCT_2:8; :: thesis: verum

end;

dom (curry f) = C by A1, Th17;
hence curry f is Function of C,(Funcs (D,E)) by A2, FUNCT_2:def 1, RELSET_1:4; :: thesis: verum