let x be Vector of V; :: according to ZMODLAT1:def 22 :: thesis: for r being Scalar of holds (f + g) . (r * x) = r * ((f + g) . x)
let r be Scalar of ; :: thesis: (f + g) . (r * x) = r * ((f + g) . x)
thus (f + g) . (r * x) = (f . (r * x)) + (g . (r * x)) by HDef3
.= (r * (f . x)) + (g . (r * x)) by HDef8
.= (r * (f . x)) + (r * (g . x)) by HDef8
.= r * ((f . x) + (g . x))
.= r * ((f + g) . x) by HDef3 ; :: thesis: verum