theorem ThLin8: :: ZMODUL06:24

for V being Z_Module
for W being free Submodule of V
for I being Subset of V
for v being VECTOR of V st I is linearly-independent & Lin I = (Omega). W & v in I holds
( (Omega). W = (Lin (I \ {v})) + (Lin {v}) & (Lin (I \ {v})) /\ (Lin {v}) = (0). V & Lin (I \ {v}) is free & Lin {v} is free & v <> 0. V )