theorem :: ZMODUL06:33

for V being free finite-rank Z_Module
for W1, W2 being free finite-rank Subspace of V st V is_the_direct_sum_of W1,W2 holds
rank V = (rank W1) + (rank W2)