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