let X be RealUnitarySpace; :: thesis: for f being Function of X,REAL st f is additive & f is homogeneous holds

f " {0} is linearly-closed

let f be Function of X,REAL; :: thesis: ( f is additive & f is homogeneous implies f " {0} is linearly-closed )

assume A1: ( f is additive & f is homogeneous ) ; :: thesis: f " {0} is linearly-closed

set X1 = f " {0};

A2: for v, u being Point of X st v in f " {0} & u in f " {0} holds

v + u in f " {0}

for v being Point of X st v in f " {0} holds

r * v in f " {0}

f " {0} is linearly-closed

let f be Function of X,REAL; :: thesis: ( f is additive & f is homogeneous implies f " {0} is linearly-closed )

assume A1: ( f is additive & f is homogeneous ) ; :: thesis: f " {0} is linearly-closed

set X1 = f " {0};

A2: for v, u being Point of X st v in f " {0} & u in f " {0} holds

v + u in f " {0}

proof

for r being Real
let v, u be Point of X; :: thesis: ( v in f " {0} & u in f " {0} implies v + u in f " {0} )

assume AS1: ( v in f " {0} & u in f " {0} ) ; :: thesis: v + u in f " {0}

then ( v in the carrier of X & f . v in {0} ) by FUNCT_2:38;

then A3: f . v = 0 by TARSKI:def 1;

A4: ( u in the carrier of X & f . u in {0} ) by AS1, FUNCT_2:38;

f . (v + u) = (f . v) + (f . u) by A1, HAHNBAN:def 2

.= 0 + 0 by A3, A4, TARSKI:def 1 ;

then f . (v + u) in {0} by TARSKI:def 1;

hence v + u in f " {0} by FUNCT_2:38; :: thesis: verum

end;assume AS1: ( v in f " {0} & u in f " {0} ) ; :: thesis: v + u in f " {0}

then ( v in the carrier of X & f . v in {0} ) by FUNCT_2:38;

then A3: f . v = 0 by TARSKI:def 1;

A4: ( u in the carrier of X & f . u in {0} ) by AS1, FUNCT_2:38;

f . (v + u) = (f . v) + (f . u) by A1, HAHNBAN:def 2

.= 0 + 0 by A3, A4, TARSKI:def 1 ;

then f . (v + u) in {0} by TARSKI:def 1;

hence v + u in f " {0} by FUNCT_2:38; :: thesis: verum

for v being Point of X st v in f " {0} holds

r * v in f " {0}

proof

hence
f " {0} is linearly-closed
by A2; :: thesis: verum
let r be Real; :: thesis: for v being Point of X st v in f " {0} holds

r * v in f " {0}

let v be Point of X; :: thesis: ( v in f " {0} implies r * v in f " {0} )

assume v in f " {0} ; :: thesis: r * v in f " {0}

then A5: ( v in the carrier of X & f . v in {0} ) by FUNCT_2:38;

f . (r * v) = r * (f . v) by A1, HAHNBAN:def 3

.= r * 0 by A5, TARSKI:def 1 ;

then f . (r * v) in {0} by TARSKI:def 1;

hence r * v in f " {0} by FUNCT_2:38; :: thesis: verum

end;r * v in f " {0}

let v be Point of X; :: thesis: ( v in f " {0} implies r * v in f " {0} )

assume v in f " {0} ; :: thesis: r * v in f " {0}

then A5: ( v in the carrier of X & f . v in {0} ) by FUNCT_2:38;

f . (r * v) = r * (f . v) by A1, HAHNBAN:def 3

.= r * 0 by A5, TARSKI:def 1 ;

then f . (r * v) in {0} by TARSKI:def 1;

hence r * v in f " {0} by FUNCT_2:38; :: thesis: verum