let f be Functional of V; :: thesis: ( f is 0-preserving & f is positively_homogeneous implies f is semi-homogeneous )
assume that
A3: f is 0-preserving and
A4: f is positively_homogeneous ; :: thesis: f is semi-homogeneous
let x be VECTOR of V; :: according to HAHNBAN:def 5 :: 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 A5: r >= 0 ; :: thesis: f . (r * x) = r * (f . x)

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

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

hence f . (r * x) = f . (0. V) by RLVECT_1:10
.= r * (f . x) by A3, A6 ;
:: thesis: verum

end;

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

hence f . (r * x) = r * (f . x) by A4; :: thesis: verum

end;

end;