let y be Vector of W; ZMODLAT1:def 30 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; ZMODLAT1:def 22 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 ; (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
;
verum