let X, Y be RealLinearSpace; :: thesis: for f being Function of X,Y st f is additive & f is homogeneous holds
f " {(0. Y)} is linearly-closed
let f be Function of X,Y; :: thesis: ( f is additive & f is homogeneous implies f " {(0. Y)} is linearly-closed )
assume A1: ( f is additive & f is homogeneous ) ; :: thesis: f " {(0. Y)} is linearly-closed
set X1 = f " {(0. Y)};
A2: for v, u being Point of X st v in f " {(0. Y)} & u in f " {(0. Y)} holds
v + u in f " {(0. Y)}

proof

let v, u be Point of X; :: thesis: ( v in f " {(0. Y)} & u in f " {(0. Y)} implies v + u in f " {(0. Y)} )
assume AS1: ( v in f " {(0. Y)} & u in f " {(0. Y)} ) ; :: thesis: v + u in f " {(0. Y)}
then ( v in the carrier of X & f . v in {(0. Y)} ) by FUNCT_2:38;
then A3: f . v = 0. Y by TARSKI:def 1;
A4: ( u in the carrier of X & f . u in {(0. Y)} ) by AS1, FUNCT_2:38;
f . (v + u) = (f . v) + (f . u) by A1
.= (0. Y) + (0. Y) by A3, A4, TARSKI:def 1
.= 0. Y by RLVECT_1:4 ;
then f . (v + u) in {(0. Y)} by TARSKI:def 1;
hence v + u in f " {(0. Y)} by FUNCT_2:38; :: thesis: verum

end;

for r being Real
for v being Point of X st v in f " {(0. Y)} holds
r * v in f " {(0. Y)}

proof

let r be Real; :: thesis: for v being Point of X st v in f " {(0. Y)} holds
r * v in f " {(0. Y)}
let v be Point of X; :: thesis: ( v in f " {(0. Y)} implies r * v in f " {(0. Y)} )
assume v in f " {(0. Y)} ; :: thesis: r * v in f " {(0. Y)}
then A5: ( v in the carrier of X & f . v in {(0. Y)} ) by FUNCT_2:38;
f . (r * v) = r * (f . v) by A1, LOPBAN_1:def 5
.= r * (0. Y) by A5, TARSKI:def 1
.= 0. Y by RLVECT_1:10 ;
then f . (r * v) in {(0. Y)} by TARSKI:def 1;
hence r * v in f " {(0. Y)} by FUNCT_2:38; :: thesis: verum

end;

hence f " {(0. Y)} is linearly-closed by A2; :: thesis: verum