let g be Functional of V; :: thesis: ( g = f *' implies g is cmplxhomogeneous )
assume A1: g = f *' ; :: thesis: g is cmplxhomogeneous
let v be Vector of V; :: according to HERMITAN:def 1 :: thesis: for a being Scalar of holds g . (a * v) = (a *') * (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 HAHNBAN1:def 8
.= (r *') * ((f . v) *') by COMPLFLD:54
.= (r *') * (g . v) by A1, Def2 ; :: thesis: verum