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

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

deffunc H_{1}( 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_{1}(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 )

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

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

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

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

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

deffunc H

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

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

then P2:
BQ c= rng (f | B)
by FUNCT_1:9;
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;( 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

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