theorem LmISRank501: :: ZMODUL06:61

for V being free finite-rank Mult-cancelable Z_Module
for W1, W2 being free finite-rank Subspace of V holds (rank (W1 + W2)) + (rank (W1 /\ W2)) = (rank W1) + (rank W2)