let w be Vector of W; ZMATRLIN:def 25 FunctionalSAF ((f + g),w) is homogeneous
set Ffg = FunctionalSAF ((f + g),w);
set Ff = FunctionalSAF (f,w);
set Fg = FunctionalSAF (g,w);
let v be Vector of V; HAHNBAN1:def 8 for b1 being Element of the carrier of INT.Ring holds (FunctionalSAF ((f + g),w)) . (b1 * v) = b1 * ((FunctionalSAF ((f + g),w)) . v)
let a be Element of INT.Ring; (FunctionalSAF ((f + g),w)) . (a * v) = a * ((FunctionalSAF ((f + g),w)) . v)
thus (FunctionalSAF ((f + g),w)) . (a * v) =
((FunctionalSAF (f,w)) + (FunctionalSAF (g,w))) . (a * v)
by BLTh12
.=
((FunctionalSAF (f,w)) . (a * v)) + ((FunctionalSAF (g,w)) . (a * v))
by HAHNBAN1:def 3
.=
(a * ((FunctionalSAF (f,w)) . v)) + ((FunctionalSAF (g,w)) . (a * v))
by HAHNBAN1:def 8
.=
(a * ((FunctionalSAF (f,w)) . v)) + (a * ((FunctionalSAF (g,w)) . v))
by HAHNBAN1:def 8
.=
a * (((FunctionalSAF (f,w)) . v) + ((FunctionalSAF (g,w)) . v))
.=
a * (((FunctionalSAF (f,w)) + (FunctionalSAF (g,w))) . v)
by HAHNBAN1:def 3
.=
a * ((FunctionalSAF ((f + g),w)) . v)
by BLTh12
; verum