:: deftheorem Def4 defines ZeroLC RMOD_4:def 4 :
for R being Ring
for V being RightMod of R
for b₃ being Linear_Combination of V holds
( b₃ = ZeroLC V iff Carrier b₃ = {} );