theorem :: RLVECT_1:49

for V being RealLinearSpace
for a being Real
for v, u, w being VECTOR of V holds a * (Sum <*v,u,w*>) = ((a * v) + (a * u)) + (a * w)