let w be Vector of W; :: according to BILINEAR:def 12 :: 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 VECTSP_1:def 19 :: thesis: (FunctionalSAF ((f + g),w)) . (v + y) = ((FunctionalSAF ((f + g),w)) . v) + ((FunctionalSAF ((f + g),w)) . y)
A1: FunctionalSAF (f,w) is additive by Def12;
A2: FunctionalSAF (g,w) is additive by Def12;
thus (FunctionalSAF ((f + g),w)) . (v + y) = ((FunctionalSAF (f,w)) + (FunctionalSAF (g,w))) . (v + y) by Th12
.= ((FunctionalSAF (f,w)) . (v + y)) + ((FunctionalSAF (g,w)) . (v + y)) by HAHNBAN1:def 3
.= (((FunctionalSAF (f,w)) . v) + ((FunctionalSAF (f,w)) . y)) + ((FunctionalSAF (g,w)) . (v + y)) by A1
.= (((FunctionalSAF (f,w)) . v) + ((FunctionalSAF (f,w)) . y)) + (((FunctionalSAF (g,w)) . v) + ((FunctionalSAF (g,w)) . y)) by A2
.= ((((FunctionalSAF (f,w)) . v) + ((FunctionalSAF (f,w)) . y)) + ((FunctionalSAF (g,w)) . v)) + ((FunctionalSAF (g,w)) . y) by RLVECT_1:def 3
.= ((((FunctionalSAF (f,w)) . v) + ((FunctionalSAF (g,w)) . v)) + ((FunctionalSAF (f,w)) . y)) + ((FunctionalSAF (g,w)) . y) by RLVECT_1:def 3
.= ((((FunctionalSAF (f,w)) + (FunctionalSAF (g,w))) . v) + ((FunctionalSAF (f,w)) . y)) + ((FunctionalSAF (g,w)) . y) by HAHNBAN1:def 3
.= (((FunctionalSAF (f,w)) + (FunctionalSAF (g,w))) . v) + (((FunctionalSAF (f,w)) . y) + ((FunctionalSAF (g,w)) . y)) by RLVECT_1:def 3
.= (((FunctionalSAF (f,w)) + (FunctionalSAF (g,w))) . v) + (((FunctionalSAF (f,w)) + (FunctionalSAF (g,w))) . y) by HAHNBAN1:def 3
.= ((FunctionalSAF ((f + g),w)) . v) + (((FunctionalSAF (f,w)) + (FunctionalSAF (g,w))) . y) by Th12
.= ((FunctionalSAF ((f + g),w)) . v) + ((FunctionalSAF ((f + g),w)) . y) by Th12 ; :: thesis: verum