for R being comRing
for V being RightMod of R
for L being Linear_Combination of V holds
( L + (ZeroLC V) = L & (ZeroLC V) + L = L )