let V be free finitely-generated Z_Module; :: thesis: ex A being finite Subset of V st A is Basis of V
set p = the prime Element of INT.Ring;
set A = the Basis of V;
set AQ = { (ZMtoMQV (V, the prime Element of INT.Ring,u)) where u is Vector of V : u in the Basis of V } ;

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

let x be object ; :: thesis: ( x in { (ZMtoMQV (V, the prime Element of INT.Ring,u)) where u is Vector of V : u in the Basis of V } implies x in the carrier of (Z_MQ_VectSp (V, the prime Element of INT.Ring)) )
assume x in { (ZMtoMQV (V, the prime Element of INT.Ring,u)) where u is Vector of V : u in the Basis of V } ; :: thesis: x in the carrier of (Z_MQ_VectSp (V, the prime Element of INT.Ring))
then consider v being Vector of V such that
B1: ( x = ZMtoMQV (V, the prime Element of INT.Ring,v) & v in the Basis of V ) ;
thus x in the carrier of (Z_MQ_VectSp (V, the prime Element of INT.Ring)) by B1; :: thesis: verum

end;

then reconsider AQ = { (ZMtoMQV (V, the prime Element of INT.Ring,u)) where u is Vector of V : u in the Basis of V } as Subset of (Z_MQ_VectSp (V, the prime Element of INT.Ring)) by TARSKI:def 3;
reconsider AQ = AQ as Basis of (Z_MQ_VectSp (V, the prime Element of INT.Ring)) by ZMODUL03:35;
consider B being finite Subset of V such that
P1: Lin B = ModuleStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) by ZMODUL03:def 4;
set BQ = { (ZMtoMQV (V, the prime Element of INT.Ring,u)) where u is Vector of V : u in B } ;

now :: thesis: for x being object st x in { (ZMtoMQV (V, the prime Element of INT.Ring,u)) where u is Vector of V : u in B } holds
x in the carrier of (Z_MQ_VectSp (V, the prime Element of INT.Ring))

let x be object ; :: thesis: ( x in { (ZMtoMQV (V, the prime Element of INT.Ring,u)) where u is Vector of V : u in B } implies x in the carrier of (Z_MQ_VectSp (V, the prime Element of INT.Ring)) )
assume x in { (ZMtoMQV (V, the prime Element of INT.Ring,u)) where u is Vector of V : u in B } ; :: thesis: x in the carrier of (Z_MQ_VectSp (V, the prime Element of INT.Ring))
then consider v being Vector of V such that
B1: ( x = ZMtoMQV (V, the prime Element of INT.Ring,v) & v in B ) ;
thus x in the carrier of (Z_MQ_VectSp (V, the prime Element of INT.Ring)) by B1; :: thesis: verum

end;

then reconsider BQ = { (ZMtoMQV (V, the prime Element of INT.Ring,u)) where u is Vector of V : u in B } as Subset of (Z_MQ_VectSp (V, the prime Element of INT.Ring)) by TARSKI:def 3;
deffunc H₁( Element of V) -> Element of the carrier of (Z_MQ_VectSp (V, the prime Element of INT.Ring)) = ZMtoMQV (V, the prime Element of INT.Ring,$1);
consider f being Function of the carrier of V,(Z_MQ_VectSp (V, the prime Element of INT.Ring)) such that
P6: for x being Element of V holds f . x = H₁(x) from FUNCT_2:sch 4();
B c= the carrier of V ;
then P8: B c= dom f by FUNCT_2:def 1;
for y being object st y in BQ holds
ex x being object st
( x in dom (f | B) & y = (f | B) . x )

proof

let y be object ; :: thesis: ( y in BQ implies ex x being object st
( x in dom (f | B) & y = (f | B) . x ) )
assume Q1: y in BQ ; :: thesis: ex x being object st
( x in dom (f | B) & y = (f | B) . x )
consider x being Vector of V such that
Q2: ( y = ZMtoMQV (V, the prime Element of INT.Ring,x) & x in B ) by Q1;
Q3: x in dom (f | B) by P8, Q2, RELAT_1:62;
Q4: y = f . x by P6, Q2
.= (f | B) . x by Q3, FUNCT_1:47 ;
take x ; :: thesis: ( x in dom (f | B) & y = (f | B) . x )
thus ( x in dom (f | B) & y = (f | B) . x ) by P8, Q2, Q4, RELAT_1:62; :: thesis: verum

end;

then P2: BQ c= rng (f | B) by FUNCT_1:9;
Lin BQ = ModuleStr(# the carrier of (Z_MQ_VectSp (V, the prime Element of INT.Ring)), the addF of (Z_MQ_VectSp (V, the prime Element of INT.Ring)), the ZeroF of (Z_MQ_VectSp (V, the prime Element of INT.Ring)), the lmult of (Z_MQ_VectSp (V, the prime Element of INT.Ring)) #) by P1, ThQuotBasis5;
then consider IQ being Basis of (Z_MQ_VectSp (V, the prime Element of INT.Ring)) such that
P4: IQ c= BQ by VECTSP_7:20;
P5: AQ is finite by P2, P4, MATRLIN:def 1, VECTSP_9:20;
card the Basis of V = card AQ by ZMODUL03:26;
then the Basis of V is finite by P5;
hence ex A being finite Subset of V st A is Basis of V ; :: thesis: verum