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

let f be Function of X,REAL; :: thesis: ( f is additive & f is homogeneous implies f " is linearly-closed )
assume A1: ( f is additive & f is homogeneous ) ; :: thesis:
set X1 = f " ;
A2: for v, u being Point of X st v in f " & u in f " holds
v + u in f "
proof
let v, u be Point of X; :: thesis: ( v in f " & u in f " implies v + u in f " )
assume AS1: ( v in f " & u in f " ) ; :: thesis: v + u in f "
then ( v in the carrier of X & f . v in ) by FUNCT_2:38;
then A3: f . v = 0 by TARSKI:def 1;
A4: ( u in the carrier of X & f . u in ) by ;
f . (v + u) = (f . v) + (f . u) by
.= 0 + 0 by ;
then f . (v + u) in by TARSKI:def 1;
hence v + u in f " by FUNCT_2:38; :: thesis: verum
end;
for r being Real
for v being Point of X st v in f " holds
r * v in f "
proof
let r be Real; :: thesis: for v being Point of X st v in f " holds
r * v in f "

let v be Point of X; :: thesis: ( v in f " implies r * v in f " )
assume v in f " ; :: thesis: r * v in f "
then A5: ( v in the carrier of X & f . v in ) by FUNCT_2:38;
f . (r * v) = r * (f . v) by
.= r * 0 by ;
then f . (r * v) in by TARSKI:def 1;
hence r * v in f " by FUNCT_2:38; :: thesis: verum
end;
hence f " is linearly-closed by A2; :: thesis: verum