let w be Vector of W; :: according to BILINEAR:def 14 :: 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 8 :: 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 Th12
.= ((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)) by VECTSP_1:def 2
.= a * (((FunctionalSAF (f,w)) + (FunctionalSAF (g,w))) . v) by HAHNBAN1:def 3
.= a * ((FunctionalSAF ((f + g),w)) . v) by Th12 ; :: thesis: verum