let f be Functional of V; :: thesis: ( f is homogeneous implies f is positively_homogeneous )
assume A2: f is 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) )
thus ( r > 0 implies f . (r * x) = r * (f . x) ) by A2, Def5; :: thesis: verum