theorem ThDirectSum: :: ZMODUL04:31

for V being Z_Module
for W1, W2 being free Subspace of V st W1 /\ W2 = (0). V holds
W1 + W2 is free