let v be Vector of V; :: according to BILINEAR:def 13 :: 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 8 :: 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 Th24;
hence (FunctionalFAF ((FormFunctional (f,g)),v)) . (r * y) = (f . v) * (g . (r * y)) by HAHNBAN1:def 6
.= (f . v) * (r * (g . y)) by HAHNBAN1:def 8
.= r * ((f . v) * (g . y)) by GROUP_1:def 3
.= r * ((FunctionalFAF ((FormFunctional (f,g)),v)) . y) by A1, HAHNBAN1:def 6 ;
:: thesis: verum