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_{1} being Element of the carrier of F_Complex holds g . (b_{1} * v) = b_{1} * (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

assume A1: g = f *' ; :: thesis: g is homogeneous

let v be Vector of V; :: according to HAHNBAN1:def 8 :: thesis: for b

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