for p being prime Element of INT.Ring
for V being free Z_Module st Z_MQ_VectSp (V,p) is finite-dimensional holds
V is finite-rank