let y be Vector of W; :: according to ZMATRLIN:def 25 :: 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 INT.Ring holds (FunctionalSAF ((FormFunctional (f,g)),y)) . (b₁ * v) = b₁ * ((FunctionalSAF ((FormFunctional (f,g)),y)) . v)
let r be Element of INT.Ring; :: 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 BLTh25;
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))
.= r * ((FunctionalSAF ((FormFunctional (f,g)),y)) . v) by A1, HAHNBAN1:def 6 ;
:: thesis: verum