let p be 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
let V be free Z_Module; ( Z_MQ_VectSp (V,p) is finite-dimensional implies V is finite-rank )
assume A1:
Z_MQ_VectSp (V,p) is finite-dimensional
; V is finite-rank
set I = the Basis of V;
set IQ = { (ZMtoMQV (V,p,u)) where u is Vector of V : u in the Basis of V } ;
then reconsider IQ = { (ZMtoMQV (V,p,u)) where u is Vector of V : u in the Basis of V } as Subset of (Z_MQ_VectSp (V,p)) by TARSKI:def 3;
A3:
IQ is Basis of (Z_MQ_VectSp (V,p))
by ZMODUL03:35;
A2:
card IQ = card the Basis of V
by ZMODUL03:26;
IQ is finite
by A1, A3, VECTSP_9:20;
then
the Basis of V is finite
by A2;
hence
V is finite-rank
by ZMODUL03:def 3; verum