let v be Vector of ; :: 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, y' be Vector of ; :: according to HAHNBAN1:def 11 :: thesis: (FunctionalFAF (FormFunctional f,g),v) . (y + y') = ((FunctionalFAF (FormFunctional f,g),v) . y) + ((FunctionalFAF (FormFunctional f,g),v) . y')
A1: FunctionalFAF (FormFunctional f,g),v = (f . v) * g by Th25;
hence (FunctionalFAF (FormFunctional f,g),v) . (y + y') = (f . v) * (g . (y + y')) by HAHNBAN1:def 9
.= (f . v) * ((g . y) + (g . y')) by HAHNBAN1:def 11
.= ((f . v) * (g . y)) + ((f . v) * (g . y')) by VECTSP_1:def 11
.= ((f . v) * (g . y)) + ((FunctionalFAF (FormFunctional f,g),v) . y') by A1, HAHNBAN1:def 9
.= ((FunctionalFAF (FormFunctional f,g),v) . y) + ((FunctionalFAF (FormFunctional f,g),v) . y') by A1, HAHNBAN1:def 9 ;
:: thesis: verum