theorem :: ZMODUL06:64

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