let V be free finite-rank Z_Module; for A being Subset of V st A is linearly-independent holds
ex B being finite Subset of V ex a being Element of INT.Ring st
( a <> 0. INT.Ring & A c= B & B is linearly-independent & ( for v being VECTOR of V holds a * v in Lin B ) )
let A be Subset of V; ( A is linearly-independent implies ex B being finite Subset of V ex a being Element of INT.Ring st
( a <> 0. INT.Ring & A c= B & B is linearly-independent & ( for v being VECTOR of V holds a * v in Lin B ) ) )
assume
A is linearly-independent
; ex B being finite Subset of V ex a being Element of INT.Ring st
( a <> 0. INT.Ring & A c= B & B is linearly-independent & ( for v being VECTOR of V holds a * v in Lin B ) )
then consider B being Subset of V such that
P1:
A c= B
and
P2:
B is linearly-independent
and
P3:
for v being VECTOR of V ex a being Element of INT.Ring st
( a <> 0. INT.Ring & a * v in Lin B )
by LmTF1;
reconsider B = B as finite Subset of V by P2;
consider I being finite Subset of V such that
A1:
I is Basis of V
by ZMODUL03:def 3;
A2:
( I is linearly-independent & Lin I = (Omega). V )
by A1, VECTSP_7:def 3;
for v being VECTOR of V st v in I holds
ex a being Element of INT.Ring st
( a <> 0. INT.Ring & a * v in Lin B )
by P3;
then consider a being Element of INT.Ring such that
B1:
a <> 0. INT.Ring
and
B2:
for v being VECTOR of V st v in I holds
a * v in Lin B
by LmTF1C;
take
B
; ex a being Element of INT.Ring st
( a <> 0. INT.Ring & A c= B & B is linearly-independent & ( for v being VECTOR of V holds a * v in Lin B ) )
take
a
; ( a <> 0. INT.Ring & A c= B & B is linearly-independent & ( for v being VECTOR of V holds a * v in Lin B ) )
thus
( a <> 0. INT.Ring & A c= B & B is linearly-independent )
by P1, B1, P2; for v being VECTOR of V holds a * v in Lin B
thus
for v being VECTOR of V holds a * v in Lin B
verum