let y be Vector of W; :: according to ZMATRLIN:def 23 :: thesis: FunctionalSAF ((FormFunctional (f,g)),y) is additive
set fg = FormFunctional (f,g);
set F = FunctionalSAF ((FormFunctional (f,g)),y);
FunctionalSAF ((FormFunctional (f,g)),y) = (g . y) * f by BLTh25;
hence FunctionalSAF ((FormFunctional (f,g)),y) is additive ; :: thesis: verum