let f be Functional of V; :: thesis: ( f is 0-preserving & f is positively_homogeneous implies f is semi-homogeneous )
assume that
A6: f is 0-preserving and
A7: f is positively_homogeneous ; :: thesis: f is semi-homogeneous
let x be VECTOR of V; :: according to HAHNBAN:def 7 :: thesis: for r being Real st r >= 0 holds
f . (r * x) = r * (f . x)
let r be Real; :: thesis: ( r >= 0 implies f . (r * x) = r * (f . x) )
assume A8: r >= 0 ; :: thesis: f . (r * x) = r * (f . x)

per cases ( r = 0 or r > 0 ) by A8;

suppose A9: r = 0 ; :: thesis: f . (r * x) = r * (f . x)

hence f . (r * x) = f . (0. V) by RLVECT_1:23
.= r * (f . x) by A6, A9, Def9 ;
:: thesis: verum

end;

suppose r > 0 ; :: thesis: f . (r * x) = r * (f . x)

hence f . (r * x) = r * (f . x) by A7, Def6; :: thesis: verum

end;

end;