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