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

reconsider I = the Basis of V as Subset of V ;

reconsider IQ = (MorphsZQ V) .: I as Subset of (Z_MQ_VectSp V) ;

A1: IQ is Basis of (Z_MQ_VectSp V) by ThEQRZMV3D;

thus rank V = card I by ZMODUL03:def 5

.= card IQ by ThEQRZMV3E

.= dim (Z_MQ_VectSp V) by A1, VECTSP_9:def 1 ; :: thesis: verum

reconsider I = the Basis of V as Subset of V ;

reconsider IQ = (MorphsZQ V) .: I as Subset of (Z_MQ_VectSp V) ;

A1: IQ is Basis of (Z_MQ_VectSp V) by ThEQRZMV3D;

thus rank V = card I by ZMODUL03:def 5

.= card IQ by ThEQRZMV3E

.= dim (Z_MQ_VectSp V) by A1, VECTSP_9:def 1 ; :: thesis: verum