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

proof

let v, u be Point of Y; :: thesis: ( v in rng f & u in rng f implies v + u in rng f )
assume A3: ( v in rng f & u in rng f ) ; :: thesis: v + u in rng f
then consider x1 being Element of the carrier of X such that
A4: v = f . x1 by FUNCT_2:113;
consider x2 being Element of the carrier of X such that
A5: u = f . x2 by A3, FUNCT_2:113;
v + u = f . (x1 + x2) by A1, A4, A5;
hence v + u in rng f by FUNCT_2:4; :: thesis: verum

end;

for r being Real
for v being Point of Y st v in rng f holds
r * v in rng f

proof

let r be Real; :: thesis: for v being Point of Y st v in rng f holds
r * v in rng f
let v be Point of Y; :: thesis: ( v in rng f implies r * v in rng f )
assume v in rng f ; :: thesis: r * v in rng f
then consider x being Element of the carrier of X such that
A6: v = f . x by FUNCT_2:113;
r * v = f . (r * x) by A1, A6, LOPBAN_1:def 5;
hence r * v in rng f by FUNCT_2:4; :: thesis: verum

end;

hence rng f is linearly-closed by A2; :: thesis: verum