theorem :: ZMODUL05:58

for V being Z_Module
for X being Subset of V st X is linearly-dependent holds
ex l being Linear_Combination of X st
( Carrier l <> {} & Sum l = 0. V ) ;