let w be Vector of W; :: according to ZMODLAT1:def 28 :: thesis: FrFunctionalSAF ((f + g),w) is additive
set Ffg = FrFunctionalSAF ((f + g),w);
set Ff = FrFunctionalSAF (f,w);
set Fg = FrFunctionalSAF (g,w);
let v, y be Vector of V; :: according to VECTSP_1:def 19 :: thesis: (FrFunctionalSAF ((f + g),w)) . (v + y) = ((FrFunctionalSAF ((f + g),w)) . v) + ((FrFunctionalSAF ((f + g),w)) . y)
A1: FrFunctionalSAF (f,w) is additive ;
A2: FrFunctionalSAF (g,w) is additive ;
thus (FrFunctionalSAF ((f + g),w)) . (v + y) = ((FrFunctionalSAF (f,w)) + (FrFunctionalSAF (g,w))) . (v + y) by HTh12
.= ((FrFunctionalSAF (f,w)) . (v + y)) + ((FrFunctionalSAF (g,w)) . (v + y)) by HDef3
.= (((FrFunctionalSAF (f,w)) . v) + ((FrFunctionalSAF (f,w)) . y)) + ((FrFunctionalSAF (g,w)) . (v + y)) by A1
.= (((FrFunctionalSAF (f,w)) . v) + ((FrFunctionalSAF (f,w)) . y)) + (((FrFunctionalSAF (g,w)) . v) + ((FrFunctionalSAF (g,w)) . y)) by A2
.= ((((FrFunctionalSAF (f,w)) . v) + ((FrFunctionalSAF (g,w)) . v)) + ((FrFunctionalSAF (f,w)) . y)) + ((FrFunctionalSAF (g,w)) . y)
.= ((((FrFunctionalSAF (f,w)) + (FrFunctionalSAF (g,w))) . v) + ((FrFunctionalSAF (f,w)) . y)) + ((FrFunctionalSAF (g,w)) . y) by HDef3
.= (((FrFunctionalSAF (f,w)) + (FrFunctionalSAF (g,w))) . v) + (((FrFunctionalSAF (f,w)) . y) + ((FrFunctionalSAF (g,w)) . y))
.= (((FrFunctionalSAF (f,w)) + (FrFunctionalSAF (g,w))) . v) + (((FrFunctionalSAF (f,w)) + (FrFunctionalSAF (g,w))) . y) by HDef3
.= ((FrFunctionalSAF ((f + g),w)) . v) + (((FrFunctionalSAF (f,w)) + (FrFunctionalSAF (g,w))) . y) by HTh12
.= ((FrFunctionalSAF ((f + g),w)) . v) + ((FrFunctionalSAF ((f + g),w)) . y) by HTh12 ; :: thesis: verum