theorem Th28: :: ZMODUL05:39

for R being Ring
for V being LeftMod of R
for l being Linear_Combination of V
for X being Subset of V st X misses Carrier l holds
l .: X c= {(0. R)}