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

for v being Point of Y st v in rng f holds

r * v in rng f

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

for r being Real
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;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

for v being Point of Y st v in rng f holds

r * v in rng f

proof

hence
rng f is linearly-closed
by A2; :: thesis: verum
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;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