theorem LmRank421: :: ZMODUL06:67

for V being torsion-free Z_Module
for W being free finite-rank Submodule of V
for u, v being VECTOR of V st W /\ (Lin {v}) = (0). V & (W + (Lin {u})) /\ (Lin {v}) <> (0). V holds
W /\ (Lin {u}) = (0). V