theorem ThRankDirectSum: :: ZMODUL06:32

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