theorem :: ZMODUL05:52

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