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

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rng (curry' f) or x in Funcs C,E )
assume A3: x in rng (curry' f) ; :: thesis: x in Funcs C,E
rng (curry' f) c= Funcs C,(rng f) by A1, FUNCT_5:42;
then consider g being Function such that
A4: x = g and
A5: dom g = C and
A6: rng g c= rng f by A3, FUNCT_2:def 2;
rng f c= E by RELAT_1:def 19;
then rng g c= E by A6, XBOOLE_1:1;
then ( g is Function of C,E & E <> {} ) by A5, FUNCT_2:def 1, RELSET_1:11;
hence x in Funcs C,E by A4, FUNCT_2:11; :: thesis: verum

end;

hence curry' f is Function of D,(Funcs C,E) by A2, FUNCT_2:def 1, RELSET_1:11; :: thesis: verum