theorem :: ZMODUL05:52

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