let v be Vector of V; :: according to BILINEAR:def 14 :: thesis: FunctionalFAF (f *' ),v is homogeneous
let w be Vector of W; :: according to HAHNBAN1:def 12 :: thesis: for b₁ being Element of the carrier of F_Complex holds (FunctionalFAF (f *' ),v) . (b₁ * w) = b₁ * ((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 Th30
.= ((r *' ) *' ) * ((f . v,w) *' ) by COMPLFLD:90
.= r * ((f *' ) . v,w) by Def8
.= r * ((FunctionalFAF (f *' ),v) . w) by BILINEAR:9 ; :: thesis: verum