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:9
.= (f . v,(r * w)) *' by Def8
.= (r * (f . v,w)) *' by BILINEAR:33
.= (r *' ) * ((f . v,w) *' ) by COMPLFLD:90
.= (r *' ) * ((f *' ) . v,w) by Def8
.= (r *' ) * ((FunctionalFAF (f *' ),v) . w) by BILINEAR:9 ; :: thesis: verum