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

set BQ = { (ZMtoMQV (V, the prime Element of INT.Ring,u)) where u is Vector of V : u in B } ;

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

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

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

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

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

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