theorem :: ZMODUL04:34

for V being Z_Module
for W being Submodule of V
for W1, W2 being free Submodule of V st W1 /\ W2 = (0). V & ModuleStr(# the carrier of W, the addF of W, the ZeroF of W, the lmult of W #) = W1 + W2 holds
W is free