let w be Vector of V; :: according to BILINEAR:def 12 :: thesis: FunctionalFAF (f + g),w is additive
set Ffg = FunctionalFAF (f + g),w;
set Ff = FunctionalFAF f,w;
set Fg = FunctionalFAF g,w;
A1: ( FunctionalFAF f,w is additive & FunctionalFAF g,w is additive ) by Def12;
let v, y be Vector of W; :: according to HAHNBAN1:def 11 :: thesis: (FunctionalFAF (f + g),w) . (v + y) = ((FunctionalFAF (f + g),w) . v) + ((FunctionalFAF (f + g),w) . y)
thus (FunctionalFAF (f + g),w) . (v + y) = ((FunctionalFAF f,w) + (FunctionalFAF g,w)) . (v + y) by Th14
.= ((FunctionalFAF f,w) . (v + y)) + ((FunctionalFAF g,w) . (v + y)) by HAHNBAN1:def 6
.= (((FunctionalFAF f,w) . v) + ((FunctionalFAF f,w) . y)) + ((FunctionalFAF g,w) . (v + y)) by A1, HAHNBAN1:def 11
.= (((FunctionalFAF f,w) . v) + ((FunctionalFAF f,w) . y)) + (((FunctionalFAF g,w) . v) + ((FunctionalFAF g,w) . y)) by A1, HAHNBAN1:def 11
.= ((((FunctionalFAF f,w) . v) + ((FunctionalFAF f,w) . y)) + ((FunctionalFAF g,w) . v)) + ((FunctionalFAF g,w) . y) by RLVECT_1:def 6
.= ((((FunctionalFAF f,w) . v) + ((FunctionalFAF g,w) . v)) + ((FunctionalFAF f,w) . y)) + ((FunctionalFAF g,w) . y) by RLVECT_1:def 6
.= ((((FunctionalFAF f,w) + (FunctionalFAF g,w)) . v) + ((FunctionalFAF f,w) . y)) + ((FunctionalFAF g,w) . y) by HAHNBAN1:def 6
.= (((FunctionalFAF f,w) + (FunctionalFAF g,w)) . v) + (((FunctionalFAF f,w) . y) + ((FunctionalFAF g,w) . y)) by RLVECT_1:def 6
.= (((FunctionalFAF f,w) + (FunctionalFAF g,w)) . v) + (((FunctionalFAF f,w) + (FunctionalFAF g,w)) . y) by HAHNBAN1:def 6
.= ((FunctionalFAF (f + g),w) . v) + (((FunctionalFAF f,w) + (FunctionalFAF g,w)) . y) by Th14
.= ((FunctionalFAF (f + g),w) . v) + ((FunctionalFAF (f + g),w) . y) by Th14 ; :: thesis: verum