let p be prime Element of INT.Ring; :: thesis: 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; :: thesis: ( Z_MQ_VectSp (V,p) is finite-dimensional implies V is finite-rank )
assume A1: Z_MQ_VectSp (V,p) is finite-dimensional ; :: thesis: 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 } ;

now :: thesis: for x being object st x in { (ZMtoMQV (V,p,u)) where u is Vector of V : u in the Basis of V } holds
x in the carrier of (Z_MQ_VectSp (V,p))

let x be object ; :: thesis: ( x in { (ZMtoMQV (V,p,u)) where u is Vector of V : u in the Basis of V } implies x in the carrier of (Z_MQ_VectSp (V,p)) )
assume x in { (ZMtoMQV (V,p,u)) where u is Vector of V : u in the Basis of V } ; :: thesis: x in the carrier of (Z_MQ_VectSp (V,p))
then consider v being Vector of V such that
B1: ( x = ZMtoMQV (V,p,v) & v in the Basis of V ) ;
thus x in the carrier of (Z_MQ_VectSp (V,p)) by B1; :: thesis: verum

end;

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; :: thesis: verum