for R being domRing
for V being RightMod of R
for L being Linear_Combination of V
for a being Scalar of R holds Sum (L * a) = (Sum L) * a