for V being Z_Module
for W1, W2, W3 being free finite-rank Subspace of V
for a being Element of INT.Ring st a <> 0. INT.Ring & W3 = a (*) W1 holds
rank (W3 /\ W2) = rank (W1 /\ W2)