let V be free finite-rank Z_Module; :: thesis: for A, B being Basis of V holds card A = card B
let A, B be Basis of V; :: thesis: card A = card B
set p = the prime Element of INT.Ring;
set AQ = { (ZMtoMQV (V, the prime Element of INT.Ring,u)) where u is Vector of V : u in A } ;

now :: thesis: for x being object st x in { (ZMtoMQV (V, the prime Element of INT.Ring,u)) where u is Vector of V : u in A } holds
x in the carrier of (Z_MQ_VectSp (V, the prime Element of INT.Ring))

let x be object ; :: thesis: ( x in { (ZMtoMQV (V, the prime Element of INT.Ring,u)) where u is Vector of V : u in A } implies x in the carrier of (Z_MQ_VectSp (V, the prime Element of INT.Ring)) )
assume x in { (ZMtoMQV (V, the prime Element of INT.Ring,u)) where u is Vector of V : u in A } ; :: thesis: x in the carrier of (Z_MQ_VectSp (V, the prime Element of INT.Ring))
then ex u being Vector of V st
( x = ZMtoMQV (V, the prime Element of INT.Ring,u) & u in A ) ;
hence x in the carrier of (Z_MQ_VectSp (V, the prime Element of INT.Ring)) ; :: thesis: verum

end;

then reconsider AQ = { (ZMtoMQV (V, the prime Element of INT.Ring,u)) where u is Vector of V : u in A } as Subset of (Z_MQ_VectSp (V, the prime Element of INT.Ring)) by TARSKI:def 3;
set BQ = { (ZMtoMQV (V, the prime Element of INT.Ring,u)) where u is Vector of V : u in B } ;

now :: thesis: for x being object st x in { (ZMtoMQV (V, the prime Element of INT.Ring,u)) where u is Vector of V : u in B } holds
x in the carrier of (Z_MQ_VectSp (V, the prime Element of INT.Ring))

let x be object ; :: thesis: ( x in { (ZMtoMQV (V, the prime Element of INT.Ring,u)) where u is Vector of V : u in B } implies x in the carrier of (Z_MQ_VectSp (V, the prime Element of INT.Ring)) )
assume x in { (ZMtoMQV (V, the prime Element of INT.Ring,u)) where u is Vector of V : u in B } ; :: thesis: x in the carrier of (Z_MQ_VectSp (V, the prime Element of INT.Ring))
then ex u being Vector of V st
( x = ZMtoMQV (V, the prime Element of INT.Ring,u) & u in B ) ;
hence x in the carrier of (Z_MQ_VectSp (V, the prime Element of INT.Ring)) ; :: thesis: verum

end;

then reconsider BQ = { (ZMtoMQV (V, the prime Element of INT.Ring,u)) where u is Vector of V : u in B } as Subset of (Z_MQ_VectSp (V, the prime Element of INT.Ring)) by TARSKI:def 3;
A1: card A = card AQ by Th26;
A2: card B = card BQ by Th26;
A3: AQ is Basis of (Z_MQ_VectSp (V, the prime Element of INT.Ring)) by Th35;
BQ is Basis of (Z_MQ_VectSp (V, the prime Element of INT.Ring)) by Th35;
hence card A = card B by A1, A2, A3, VECTSP_9:22; :: thesis: verum