theorem LmSumModX: :: ZMODUL06:30

for V being torsion-free Z_Module
for W being free finite-rank Subspace of V
for v being Vector of V st v <> 0. V & W /\ (Lin {v}) <> (0). V holds
W + (Lin {v}) is free