let v be Vector of V; :: according to BILINEAR:def 13 :: thesis: FunctionalFAF ((f *'),v) is homogeneous
let w be Vector of W; :: according to HAHNBAN1:def 8 :: 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:8
.= (f . (v,(r * w))) *' by Def8
.= ((r *') * (f . (v,w))) *' by Th27
.= ((r *') *') * ((f . (v,w)) *') by COMPLFLD:54
.= r * ((f *') . (v,w)) by Def8
.= r * ((FunctionalFAF ((f *'),v)) . w) by BILINEAR:8 ; :: thesis: verum