for R being Ring
for V being LeftMod of R
for L1, L2 being Linear_Combination of V
for a being Element of R holds a * (L1 + L2) = (a * L1) + (a * L2) by VECTSP_6:33;