let p be prime Element of INT.Ring; 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; 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 } ;
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;
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; verum