theorem Th9: :: RMOD_4:9

for R being Ring
for V being RightMod of R
for S, T being finite Subset of V st T misses S holds
Sum (T \/ S) = (Sum T) + (Sum S)