theorem Th21: :: RMOD_4:21

for R being Ring
for V being RightMod of R
for l being Linear_Combination of {} the carrier of V holds l = ZeroLC V