for R being Ring
for V being LeftMod of R
for L being Linear_Combination of V
for v being Element of V holds
( L . v = 0. R iff not v in Carrier L )