let v be Vector of V; :: according to BILINEAR:def 14 :: thesis: FunctionalFAF (FormFunctional f,g),v is homogeneous
set fg = FormFunctional f,g;
set F = FunctionalFAF (FormFunctional f,g),v;
let y be Vector of W; :: according to HAHNBAN1:def 12 :: thesis: for b₁ being Element of the carrier of K holds (FunctionalFAF (FormFunctional f,g),v) . (b₁ * y) = b₁ * ((FunctionalFAF (FormFunctional f,g),v) . y)
let r be Scalar of ; :: thesis: (FunctionalFAF (FormFunctional f,g),v) . (r * y) = r * ((FunctionalFAF (FormFunctional f,g),v) . y)
A1: FunctionalFAF (FormFunctional f,g),v = (f . v) * g by Th25;
hence (FunctionalFAF (FormFunctional f,g),v) . (r * y) = (f . v) * (g . (r * y)) by HAHNBAN1:def 9
.= (f . v) * (r * (g . y)) by HAHNBAN1:def 12
.= r * ((f . v) * (g . y)) by GROUP_1:def 4
.= r * ((FunctionalFAF (FormFunctional f,g),v) . y) by A1, HAHNBAN1:def 9 ;
:: thesis: verum