theorem :: ZMODUL07:9

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