theorem LmTF1: :: ZMODUL07:2

for V being Z_Module
for A being Subset of V st A is linearly-independent holds
ex B being Subset of V st
( A c= B & B is linearly-independent & ( for v being VECTOR of V ex a being Element of INT.Ring st
( a <> 0 & a * v in Lin B ) ) )