let y be Vector of W; :: according to ZMODLAT1:def 30 :: thesis: FrFunctionalSAF ((FrFormFunctional (f,g)),y) is homogeneous
set fg = FrFormFunctional (f,g);
set F = FrFunctionalSAF ((FrFormFunctional (f,g)),y);
let v be Vector of V; :: according to ZMODLAT1:def 22 :: thesis: for r being Scalar of holds (FrFunctionalSAF ((FrFormFunctional (f,g)),y)) . (r * v) = r * ((FrFunctionalSAF ((FrFormFunctional (f,g)),y)) . v)
let r be Scalar of ; :: thesis: (FrFunctionalSAF ((FrFormFunctional (f,g)),y)) . (r * v) = r * ((FrFunctionalSAF ((FrFormFunctional (f,g)),y)) . v)
A1: FrFunctionalSAF ((FrFormFunctional (f,g)),y) = (g . y) * f by HTh25;
hence (FrFunctionalSAF ((FrFormFunctional (f,g)),y)) . (r * v) = (g . y) * (f . (r * v)) by HDef6
.= (g . y) * (r * (f . v)) by HDef8
.= r * ((g . y) * (f . v))
.= r * ((FrFunctionalSAF ((FrFormFunctional (f,g)),y)) . v) by A1, HDef6 ;
:: thesis: verum