let f be Functional of V; :: thesis: ( f is semi-homogeneous implies f is positively_homogeneous )
assume A3: f is semi-homogeneous ; :: thesis: f is positively_homogeneous
let x be VECTOR of V; :: according to HAHNBAN:def 4 :: 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)
hence f . (r * x) = r * (f . x) by A3, Def7; :: thesis: verum