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 } ;

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

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))

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;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;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

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