theorem ThRankS1: :: ZMODUL06:52

for V being Z_Module
for W being free finite-rank Subspace of V
for a being Element of INT.Ring st a <> 0. INT.Ring holds
rank (a (*) W) = rank W