let f be Functional of V; :: thesis: ( f is absolutely_homogeneous implies f is semi-homogeneous )
assume A5: f is absolutely_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 r >= 0 ; :: thesis: f . (r * x) = r * (f . x)
then abs r = r by ABSVALUE:def 1;
hence f . (r * x) = r * (f . x) by A5, Def8; :: thesis: verum