let w be Vector of V; ZMATRLIN:def 22 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; VECTSP_1:def 19 (FunctionalFAF ((f + g),w)) . (v + y) = ((FunctionalFAF ((f + g),w)) . v) + ((FunctionalFAF ((f + g),w)) . y)
A1:
FunctionalFAF (f,w) is additive
;
A2:
FunctionalFAF (g,w) is additive
;
thus (FunctionalFAF ((f + g),w)) . (v + y) =
((FunctionalFAF (f,w)) + (FunctionalFAF (g,w))) . (v + y)
by BLTh13
.=
((FunctionalFAF (f,w)) . (v + y)) + ((FunctionalFAF (g,w)) . (v + y))
by HAHNBAN1:def 3
.=
(((FunctionalFAF (f,w)) . v) + ((FunctionalFAF (f,w)) . y)) + ((FunctionalFAF (g,w)) . (v + y))
by A1
.=
(((FunctionalFAF (f,w)) . v) + ((FunctionalFAF (f,w)) . y)) + (((FunctionalFAF (g,w)) . v) + ((FunctionalFAF (g,w)) . y))
by A2
.=
((((FunctionalFAF (f,w)) . v) + ((FunctionalFAF (g,w)) . v)) + ((FunctionalFAF (f,w)) . y)) + ((FunctionalFAF (g,w)) . y)
.=
((((FunctionalFAF (f,w)) + (FunctionalFAF (g,w))) . v) + ((FunctionalFAF (f,w)) . y)) + ((FunctionalFAF (g,w)) . y)
by HAHNBAN1:def 3
.=
(((FunctionalFAF (f,w)) + (FunctionalFAF (g,w))) . v) + (((FunctionalFAF (f,w)) . y) + ((FunctionalFAF (g,w)) . y))
.=
(((FunctionalFAF (f,w)) + (FunctionalFAF (g,w))) . v) + (((FunctionalFAF (f,w)) + (FunctionalFAF (g,w))) . y)
by HAHNBAN1:def 3
.=
((FunctionalFAF ((f + g),w)) . v) + (((FunctionalFAF (f,w)) + (FunctionalFAF (g,w))) . y)
by BLTh13
.=
((FunctionalFAF ((f + g),w)) . v) + ((FunctionalFAF ((f + g),w)) . y)
by BLTh13
; verum