let y be Vector of W; :: according to BILINEAR:def 12 :: 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 Th25;

hence FunctionalSAF ((FormFunctional (f,g)),y) is additive ; :: thesis: verum

set fg = FormFunctional (f,g);

set F = FunctionalSAF ((FormFunctional (f,g)),y);

FunctionalSAF ((FormFunctional (f,g)),y) = (g . y) * f by Th25;

hence FunctionalSAF ((FormFunctional (f,g)),y) is additive ; :: thesis: verum