theorem LmISRank42: :: ZMODUL06:58

for V being torsion-free Z_Module
for W1, W2 being free finite-rank Subspace of V
for I being Basis of W1 st ( for v being Vector of V st v in I holds
(W1 /\ W2) /\ (Lin {v}) <> (0). V ) holds
rank (W1 + W2) = rank W2