let v be Vector of V; :: according to HERMITAN:def 4 :: thesis: FunctionalFAF ((f *'),v) is cmplxhomogeneous

let w be Vector of W; :: according to HERMITAN:def 1 :: thesis: for a being Scalar of holds (FunctionalFAF ((f *'),v)) . (a * w) = (a *') * ((FunctionalFAF ((f *'),v)) . w)

let r be Scalar of ; :: thesis: (FunctionalFAF ((f *'),v)) . (r * w) = (r *') * ((FunctionalFAF ((f *'),v)) . w)

set fg = FunctionalFAF ((f *'),v);

thus (FunctionalFAF ((f *'),v)) . (r * w) = (f *') . (v,(r * w)) by BILINEAR:8

.= (f . (v,(r * w))) *' by Def8

.= (r * (f . (v,w))) *' by BILINEAR:32

.= (r *') * ((f . (v,w)) *') by COMPLFLD:54

.= (r *') * ((f *') . (v,w)) by Def8

.= (r *') * ((FunctionalFAF ((f *'),v)) . w) by BILINEAR:8 ; :: thesis: verum

let w be Vector of W; :: according to HERMITAN:def 1 :: thesis: for a being Scalar of holds (FunctionalFAF ((f *'),v)) . (a * w) = (a *') * ((FunctionalFAF ((f *'),v)) . w)

let r be Scalar of ; :: thesis: (FunctionalFAF ((f *'),v)) . (r * w) = (r *') * ((FunctionalFAF ((f *'),v)) . w)

set fg = FunctionalFAF ((f *'),v);

thus (FunctionalFAF ((f *'),v)) . (r * w) = (f *') . (v,(r * w)) by BILINEAR:8

.= (f . (v,(r * w))) *' by Def8

.= (r * (f . (v,w))) *' by BILINEAR:32

.= (r *') * ((f . (v,w)) *') by COMPLFLD:54

.= (r *') * ((f *') . (v,w)) by Def8

.= (r *') * ((FunctionalFAF ((f *'),v)) . w) by BILINEAR:8 ; :: thesis: verum