let y be Vector of W; :: according to ZMODLAT1:def 28 :: thesis: FrFunctionalSAF ((FrFormFunctional (f,g)),y) is additive
set fg = FrFormFunctional (f,g);
set F = FrFunctionalSAF ((FrFormFunctional (f,g)),y);
FrFunctionalSAF ((FrFormFunctional (f,g)),y) = (g . y) * f by HTh25;
hence FrFunctionalSAF ((FrFormFunctional (f,g)),y) is additive ; :: thesis: verum