theorem LmRankSX11: :: ZMODUL07:5

for V being free finite-rank Z_Module
for A being linearly-independent Subset of V ex I being finite linearly-independent Subset of V ex a being Element of INT.Ring st
( a <> 0. INT.Ring & A c= I & a (*) V is Submodule of Lin I )