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