let w be Vector of W; :: according to BILINEAR:def 13 :: thesis: FunctionalSAF (f + g),w is additive
set Ffg = FunctionalSAF (f + g),w;
set Ff = FunctionalSAF f,w;
set Fg = FunctionalSAF g,w;
let v, y be Vector of V; :: according to GRCAT_1:def 13 :: thesis: (FunctionalSAF (f + g),w) . (v + y) = ((FunctionalSAF (f + g),w) . v) + ((FunctionalSAF (f + g),w) . y)
A1: FunctionalSAF f,w is additive by Def13;
A2: FunctionalSAF g,w is additive by Def13;
thus (FunctionalSAF (f + g),w) . (v + y) = ((FunctionalSAF f,w) + (FunctionalSAF g,w)) . (v + y) by Th13
.= ((FunctionalSAF f,w) . (v + y)) + ((FunctionalSAF g,w) . (v + y)) by HAHNBAN1:def 6
.= (((FunctionalSAF f,w) . v) + ((FunctionalSAF f,w) . y)) + ((FunctionalSAF g,w) . (v + y)) by A1, GRCAT_1:def 13
.= (((FunctionalSAF f,w) . v) + ((FunctionalSAF f,w) . y)) + (((FunctionalSAF g,w) . v) + ((FunctionalSAF g,w) . y)) by A2, GRCAT_1:def 13
.= ((((FunctionalSAF f,w) . v) + ((FunctionalSAF f,w) . y)) + ((FunctionalSAF g,w) . v)) + ((FunctionalSAF g,w) . y) by RLVECT_1:def 6
.= ((((FunctionalSAF f,w) . v) + ((FunctionalSAF g,w) . v)) + ((FunctionalSAF f,w) . y)) + ((FunctionalSAF g,w) . y) by RLVECT_1:def 6
.= ((((FunctionalSAF f,w) + (FunctionalSAF g,w)) . v) + ((FunctionalSAF f,w) . y)) + ((FunctionalSAF g,w) . y) by HAHNBAN1:def 6
.= (((FunctionalSAF f,w) + (FunctionalSAF g,w)) . v) + (((FunctionalSAF f,w) . y) + ((FunctionalSAF g,w) . y)) by RLVECT_1:def 6
.= (((FunctionalSAF f,w) + (FunctionalSAF g,w)) . v) + (((FunctionalSAF f,w) + (FunctionalSAF g,w)) . y) by HAHNBAN1:def 6
.= ((FunctionalSAF (f + g),w) . v) + (((FunctionalSAF f,w) + (FunctionalSAF g,w)) . y) by Th13
.= ((FunctionalSAF (f + g),w) . v) + ((FunctionalSAF (f + g),w) . y) by Th13 ; :: thesis: verum