theorem :: RLVECT_1:48

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