let w be Vector of W; :: according to BILINEAR:def 15 :: thesis: 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; :: according to HAHNBAN1:def 12 :: thesis: for b₁ being Element of the carrier of K holds (FunctionalSAF (f + g),w) . (b₁ * v) = b₁ * ((FunctionalSAF (f + g),w) . v)
let a be Scalar of ; :: thesis: (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 Th13
.= ((FunctionalSAF f,w) . (a * v)) + ((FunctionalSAF g,w) . (a * v)) by HAHNBAN1:def 6
.= (a * ((FunctionalSAF f,w) . v)) + ((FunctionalSAF g,w) . (a * v)) by HAHNBAN1:def 12
.= (a * ((FunctionalSAF f,w) . v)) + (a * ((FunctionalSAF g,w) . v)) by HAHNBAN1:def 12
.= a * (((FunctionalSAF f,w) . v) + ((FunctionalSAF g,w) . v)) by VECTSP_1:def 11
.= a * (((FunctionalSAF f,w) + (FunctionalSAF g,w)) . v) by HAHNBAN1:def 6
.= a * ((FunctionalSAF (f + g),w) . v) by Th13 ; :: thesis: verum