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;
let v, y be Vector of W; :: according to GRCAT_1:def 13 :: thesis: (FunctionalFAF (f + g),w) . (v + y) = ((FunctionalFAF (f + g),w) . v) + ((FunctionalFAF (f + g),w) . y)
A1: FunctionalFAF f,w is additive by Def12;
A2: FunctionalFAF g,w is additive by Def12;
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, GRCAT_1:def 13
.= (((FunctionalFAF f,w) . v) + ((FunctionalFAF f,w) . y)) + (((FunctionalFAF g,w) . v) + ((FunctionalFAF g,w) . y)) by A2, GRCAT_1:def 13
.= ((((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