let y be Vector of W; :: according to BILINEAR:def 13 :: 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 Th26;
hence FunctionalSAF (FormFunctional f,g),y is additive ; :: thesis: verum