let C, D, E be non empty set ; 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; curry' f is Function of D,(Funcs (C,E))
A1:
dom f = [:C,D:]
by FUNCT_2:def 1;
A2:
rng (curry' f) c= Funcs (C,E)
proof
A3:
rng (curry' f) c= Funcs (
C,
(rng f))
by A1, Th28;
let x be
object ;
TARSKI:def 3 ( not x in rng (curry' f) or x in Funcs (C,E) )
assume
x in rng (curry' f)
;
x in Funcs (C,E)
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 g c= E
by A6, XBOOLE_1:1;
then
g is
Function of
C,
E
by A5, FUNCT_2:def 1, RELSET_1:4;
hence
x in Funcs (
C,
E)
by A4, FUNCT_2:8;
verum
end;
dom (curry' f) = D
by A1, Th17;
hence
curry' f is Function of D,(Funcs (C,E))
by A2, FUNCT_2:def 1, RELSET_1:4; verum