let p be prime Element of INT.Ring; :: thesis: for V being free finite-rank Z_Module holds rank V = dim (Z_MQ_VectSp (V,p))

let V be free finite-rank Z_Module; :: thesis: rank V = dim (Z_MQ_VectSp (V,p))

set W = Z_MQ_VectSp (V,p);

set A = the Basis of V;

set AQ = { (ZMtoMQV (V,p,u)) where u is Vector of V : u in the Basis of V } ;

A1: card the Basis of V = card AQ by Th26;

AQ is Basis of (Z_MQ_VectSp (V,p)) by Th35;

then dim (Z_MQ_VectSp (V,p)) = card AQ by VECTSP_9:def 1;

hence rank V = dim (Z_MQ_VectSp (V,p)) by A1, Def5; :: thesis: verum

let V be free finite-rank Z_Module; :: thesis: rank V = dim (Z_MQ_VectSp (V,p))

set W = Z_MQ_VectSp (V,p);

set A = the Basis of V;

set AQ = { (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 AQ = { (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 ex u being Vector of V st

( x = ZMtoMQV (V,p,u) & u in the Basis of V ) ;

hence x in the carrier of (Z_MQ_VectSp (V,p)) ; :: 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 ex u being Vector of V st

( x = ZMtoMQV (V,p,u) & u in the Basis of V ) ;

hence x in the carrier of (Z_MQ_VectSp (V,p)) ; :: thesis: verum

A1: card the Basis of V = card AQ by Th26;

AQ is Basis of (Z_MQ_VectSp (V,p)) by Th35;

then dim (Z_MQ_VectSp (V,p)) = card AQ by VECTSP_9:def 1;

hence rank V = dim (Z_MQ_VectSp (V,p)) by A1, Def5; :: thesis: verum