let w be Vector of V; :: according to ZMODLAT1:def 29 :: thesis: FrFunctionalFAF ((f + g),w) is homogeneous
set Ffg = FrFunctionalFAF ((f + g),w);
set Ff = FrFunctionalFAF (f,w);
set Fg = FrFunctionalFAF (g,w);
let v be Vector of W; :: according to ZMODLAT1:def 22 :: thesis: for r being Scalar of holds (FrFunctionalFAF ((f + g),w)) . (r * v) = r * ((FrFunctionalFAF ((f + g),w)) . v)
let a be Scalar of ; :: thesis: (FrFunctionalFAF ((f + g),w)) . (a * v) = a * ((FrFunctionalFAF ((f + g),w)) . v)
thus (FrFunctionalFAF ((f + g),w)) . (a * v) = ((FrFunctionalFAF (f,w)) + (FrFunctionalFAF (g,w))) . (a * v) by HTh13
.= ((FrFunctionalFAF (f,w)) . (a * v)) + ((FrFunctionalFAF (g,w)) . (a * v)) by HDef3
.= (a * ((FrFunctionalFAF (f,w)) . v)) + ((FrFunctionalFAF (g,w)) . (a * v)) by HDef8
.= (a * ((FrFunctionalFAF (f,w)) . v)) + (a * ((FrFunctionalFAF (g,w)) . v)) by HDef8
.= a * (((FrFunctionalFAF (f,w)) . v) + ((FrFunctionalFAF (g,w)) . v))
.= a * (((FrFunctionalFAF (f,w)) + (FrFunctionalFAF (g,w))) . v) by HDef3
.= a * ((FrFunctionalFAF ((f + g),w)) . v) by HTh13 ; :: thesis: verum