theorem :: ZMODUL04:16

for V being free finite-rank Z_Module holds rank V = dim (Z_MQ_VectSp V)