let x be Vector of V; :: according to HAHNBAN1:def 8 :: 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 Def3
.= (r * (f . x)) + (g . (r * x)) by Def8
.= (r * (f . x)) + (r * (g . x)) by Def8
.= r * ((f . x) + (g . x)) by VECTSP_1:def 2
.= r * ((f + g) . x) by Def3 ; :: thesis: verum