theorem :: ZMODUL07:8

for V being torsion-free Z_Module
for W1, W2 being free finite-rank Submodule of V st W2 is Submodule of W1 holds
ex W3 being free finite-rank Submodule of V st
( rank W1 = (rank W2) + (rank W3) & W2 /\ W3 = (0). V & W3 is Submodule of W1 )