theorem Th13: :: RMOD_4:13
for R being Ring
for V being RightMod of R
for S, T being finite Subset of V holds Sum (T \ S) = (Sum T) - (Sum (T /\ S))