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 } ;

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

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))

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;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;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

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