let v be Vector of V; :: according to BILINEAR:def 12 :: thesis: FunctionalFAF ((FormFunctional (f,g)),v) is additive
set fg = FormFunctional (f,g);
set F = FunctionalFAF ((FormFunctional (f,g)),v);
let y, y9 be Vector of W; :: according to GRCAT_1:def 13 :: thesis: (FunctionalFAF ((FormFunctional (f,g)),v)) . (y + y9) = ((FunctionalFAF ((FormFunctional (f,g)),v)) . y) + ((FunctionalFAF ((FormFunctional (f,g)),v)) . y9)
A1: FunctionalFAF ((FormFunctional (f,g)),v) = (f . v) * g by Th25;
hence (FunctionalFAF ((FormFunctional (f,g)),v)) . (y + y9) = (f . v) * (g . (y + y9)) by HAHNBAN1:def 9
.= (f . v) * ((g . y) + (g . y9)) by GRCAT_1:def 13
.= ((f . v) * (g . y)) + ((f . v) * (g . y9)) by VECTSP_1:def 11
.= ((f . v) * (g . y)) + ((FunctionalFAF ((FormFunctional (f,g)),v)) . y9) by A1, HAHNBAN1:def 9
.= ((FunctionalFAF ((FormFunctional (f,g)),v)) . y) + ((FunctionalFAF ((FormFunctional (f,g)),v)) . y9) by A1, HAHNBAN1:def 9 ;
:: thesis: verum