for R being comRing
for V being RightMod of R
for L1, L2 being Linear_Combination of V holds L1 + L2 = L2 + L1