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