theorem :: ZMODUL02:54
for R being Ring
for V being LeftMod of R
for L being Linear_Combination of V holds Sum (- L) = - (Sum L) by VECTSP_6:46;