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

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