consider I being finite Subset of V such that

P1: I is Basis of V by ZMODUL03:def 3;

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

IQ is Basis of (Z_MQ_VectSp V) by P1, ThEQRZMV3D;

hence Z_MQ_VectSp V is finite-dimensional by MATRLIN:def 1; :: thesis: verum

P1: I is Basis of V by ZMODUL03:def 3;

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

IQ is Basis of (Z_MQ_VectSp V) by P1, ThEQRZMV3D;

hence Z_MQ_VectSp V is finite-dimensional by MATRLIN:def 1; :: thesis: verum