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