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