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