theorem LmRank2: :: ZMODUL06:38

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
rank (W + (Lin {v})) = rank W