set W = Z_MQ_VectSp (V,p);
set A = the Basis of V;
set AQ = { (ZMtoMQV (V,p,u)) where u is Vector of V : u in the Basis of V } ;

now :: thesis: for x being object st x in { (ZMtoMQV (V,p,u)) where u is Vector of V : u in the Basis of V } holds
x in the carrier of (Z_MQ_VectSp (V,p))

let x be object ; :: thesis: ( x in { (ZMtoMQV (V,p,u)) where u is Vector of V : u in the Basis of V } implies x in the carrier of (Z_MQ_VectSp (V,p)) )
assume x in { (ZMtoMQV (V,p,u)) where u is Vector of V : u in the Basis of V } ; :: thesis: x in the carrier of (Z_MQ_VectSp (V,p))
then ex u being Vector of V st
( x = ZMtoMQV (V,p,u) & u in the Basis of V ) ;
hence x in the carrier of (Z_MQ_VectSp (V,p)) ; :: thesis: verum

end;

then reconsider AQ = { (ZMtoMQV (V,p,u)) where u is Vector of V : u in the Basis of V } as Subset of (Z_MQ_VectSp (V,p)) by TARSKI:def 3;
card the Basis of V = card AQ by Th26;
then AQ is finite Subset of (Z_MQ_VectSp (V,p)) ;
hence Z_MQ_VectSp (V,p) is finite-dimensional by Th35, MATRLIN:def 1; :: thesis: verum