let g be Functional of V; :: thesis: ( g = f *' implies g is homogeneous )
assume A1: g = f *' ; :: thesis: g is homogeneous
let v be Vector of V; :: according to HAHNBAN1:def 8 :: thesis: for b₁ being Element of the carrier of F_Complex holds g . (b₁ * v) = b₁ * (g . v)
let r be Scalar of ; :: thesis: g . (r * v) = r * (g . v)
thus g . (r * v) = (f . (r * v)) *' by A1, Def2
.= ((r *') * (f . v)) *' by Def1
.= ((r *') *') * ((f . v) *') by COMPLFLD:54
.= r * (g . v) by A1, Def2 ; :: thesis: verum