let y be Vector of W; :: according to BILINEAR:def 15 :: 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 12 :: 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 Th26;
hence (FunctionalSAF (FormFunctional f,g),y) . (r * v) = (g . y) * (f . (r * v)) by HAHNBAN1:def 9
.= (g . y) * (r * (f . v)) by HAHNBAN1:def 12
.= r * ((g . y) * (f . v)) by GROUP_1:def 4
.= r * ((FunctionalSAF (FormFunctional f,g),y) . v) by A1, HAHNBAN1:def 9 ;
:: thesis: verum