let V be Z_Module; :: thesis: for A being Subset of V st A is linearly-independent holds
ex B being Subset of V st
( A c= B & B is linearly-independent & ( for v being VECTOR of V ex a being Element of INT.Ring st
( a <> 0 & a * v in Lin B ) ) )
let A be Subset of V; :: thesis: ( A is linearly-independent implies ex B being Subset of V st
( A c= B & B is linearly-independent & ( for v being VECTOR of V ex a being Element of INT.Ring st
( a <> 0 & a * v in Lin B ) ) ) )
assume A1: A is linearly-independent ; :: thesis: ex B being Subset of V st
( A c= B & B is linearly-independent & ( for v being VECTOR of V ex a being Element of INT.Ring st
( a <> 0 & a * v in Lin B ) ) )
defpred S₁[ set ] means ex B being Subset of V st
( B = $1 & A c= B & B is linearly-independent );
consider Q being set such that
A2: for Z being set holds
( Z in Q iff ( Z in bool the carrier of V & S₁[Z] ) ) from XFAMILY:sch 1();

A3: now :: thesis: for Z being set st Z <> {} & Z c= Q & Z is c=-linear holds
union Z in Q

let Z be set ; :: thesis: ( Z <> {} & Z c= Q & Z is c=-linear implies union Z in Q )
assume that
A4: Z <> {} and
A5: Z c= Q and
A6: Z is c=-linear ; :: thesis: union Z in Q
set W = union Z;
union Z c= the carrier of V

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in union Z or x in the carrier of V )
assume x in union Z ; :: thesis: x in the carrier of V
then consider X being set such that
A7: x in X and
A8: X in Z by TARSKI:def 4;
X in bool the carrier of V by A2, A5, A8;
hence x in the carrier of V by A7; :: thesis: verum

end;

then reconsider W = union Z as Subset of V ;
A9: W is linearly-independent

proof

deffunc H₁( object ) -> set = { C where C is Subset of V : ( $1 in C & C in Z ) } ;
let l be Linear_Combination of W; :: according to VECTSP_7:def 1 :: thesis: ( not Sum l = 0. V or Carrier l = {} )
assume that
A10: Sum l = 0. V and
A11: Carrier l <> {} ; :: thesis: contradiction
consider f being Function such that
A12: dom f = Carrier l and
A13: for x being object st x in Carrier l holds
f . x = H₁(x) from FUNCT_1:sch 3();
reconsider M = rng f as non empty set by A11, A12, RELAT_1:42;
set F = the Choice_Function of M;
set S = rng the Choice_Function of M;

A14: now :: thesis: not {} in M

assume {} in M ; :: thesis: contradiction
then consider x being object such that
A15: x in dom f and
A16: f . x = {} by FUNCT_1:def 3;
Carrier l c= W by VECTSP_6:def 4;
then consider X being set such that
A17: x in X and
A18: X in Z by A12, A15, TARSKI:def 4;
reconsider X = X as Subset of V by A2, A5, A18;
X in { C where C is Subset of V : ( x in C & C in Z ) } by A17, A18;
hence contradiction by A12, A13, A15, A16; :: thesis: verum

end;

then A19: dom the Choice_Function of M = M by RLVECT_3:28;
then dom the Choice_Function of M is finite by A12, FINSET_1:8;
then A20: rng the Choice_Function of M is finite by FINSET_1:8;

A21: now :: thesis: for X being set st X in rng the Choice_Function of M holds
X in Z

let X be set ; :: thesis: ( X in rng the Choice_Function of M implies X in Z )
assume X in rng the Choice_Function of M ; :: thesis: X in Z
then consider x being object such that
A22: x in dom the Choice_Function of M and
A23: the Choice_Function of M . x = X by FUNCT_1:def 3;
consider y being object such that
A24: ( y in dom f & f . y = x ) by A22, FUNCT_1:def 3;
reconsider x = x as set by TARSKI:1;
A25: x = H₁(y) by A12, A13, A24;
X in x by A14, A22, A23, ORDERS_1:89;
then ex C being Subset of V st
( C = X & y in C & C in Z ) by A25;
hence X in Z ; :: thesis: verum

end;

A26: now :: thesis: for X, Y being set st X in rng the Choice_Function of M & Y in rng the Choice_Function of M & not X c= Y holds
Y c= X

let X, Y be set ; :: thesis: ( X in rng the Choice_Function of M & Y in rng the Choice_Function of M & not X c= Y implies Y c= X )
assume ( X in rng the Choice_Function of M & Y in rng the Choice_Function of M ) ; :: thesis: ( X c= Y or Y c= X )
then ( X in Z & Y in Z ) by A21;
hence ( X c= Y or Y c= X ) by A6, ORDINAL1:def 8, XBOOLE_0:def 9; :: thesis: verum

end;

rng the Choice_Function of M <> {} by A19, RELAT_1:42;
then union (rng the Choice_Function of M) in Z by A20, A21, A26, CARD_2:62;
then consider B being Subset of V such that
A27: B = union (rng the Choice_Function of M) and
A c= B and
A28: B is linearly-independent by A2, A5;
Carrier l c= union (rng the Choice_Function of M)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Carrier l or x in union (rng the Choice_Function of M) )
set X = f . x;
assume A29: x in Carrier l ; :: thesis: x in union (rng the Choice_Function of M)
then A30: f . x = { C where C is Subset of V : ( x in C & C in Z ) } by A13;
A31: f . x in M by A12, A29, FUNCT_1:def 3;
then the Choice_Function of M . (f . x) in f . x by A14, ORDERS_1:89;
then A32: ex C being Subset of V st
( the Choice_Function of M . (f . x) = C & x in C & C in Z ) by A30;
the Choice_Function of M . (f . x) in rng the Choice_Function of M by A19, A31, FUNCT_1:def 3;
hence x in union (rng the Choice_Function of M) by A32, TARSKI:def 4; :: thesis: verum

end;

then l is Linear_Combination of B by A27, VECTSP_6:def 4;
hence contradiction by A10, A11, A28; :: thesis: verum

end;

set x = the Element of Z;
the Element of Z in Q by A4, A5;
then A33: ex B being Subset of V st
( B = the Element of Z & A c= B & B is linearly-independent ) by A2;
the Element of Z c= W by A4, ZFMISC_1:74;
hence union Z in Q by A2, A9, A33, XBOOLE_1:1; :: thesis: verum

end;

Q <> {} by A1, A2;
then consider X being set such that
A34: X in Q and
A35: for Z being set st Z in Q & Z <> X holds
not X c= Z by A3, ORDERS_1:67;
consider B being Subset of V such that
A36: B = X and
A37: A c= B and
A38: B is linearly-independent by A2, A34;
take B ; :: thesis: ( A c= B & B is linearly-independent & ( for v being VECTOR of V ex a being Element of INT.Ring st
( a <> 0 & a * v in Lin B ) ) )
thus ( A c= B & B is linearly-independent ) by A37, A38; :: thesis: for v being VECTOR of V ex a being Element of INT.Ring st
( a <> 0 & a * v in Lin B )
assume ex v being VECTOR of V st
for a being Element of INT.Ring holds
( not a <> 0 or not a * v in Lin B ) ; :: thesis: contradiction
then consider v being VECTOR of V such that
A39: for a being Element of INT.Ring st a <> 0 holds
not a * v in Lin B ;
A40: B \/ {v} is linearly-independent

proof

let l be Linear_Combination of B \/ {v}; :: according to VECTSP_7:def 1 :: thesis: ( not Sum l = 0. V or Carrier l = {} )
assume A41: Sum l = 0. V ; :: thesis: Carrier l = {}

now :: thesis: Carrier l = {}

per cases ( v in Carrier l or not v in Carrier l ) ;

suppose B1: v in Carrier l ; :: thesis: Carrier l = {}

reconsider i0 = 0 as Element of INT.Ring ;
deffunc H₁( VECTOR of V) -> Element of INT.Ring = i0;
deffunc H₂( VECTOR of V) -> Element of the carrier of INT.Ring = l . $1;
consider f being Function of V,INT.Ring such that
A42: f . v = i0 and
A43: for u being VECTOR of V st u <> v holds
f . u = H₂(u) from FUNCT_2:sch 6();
reconsider f = f as Element of Funcs ( the carrier of V, the carrier of INT.Ring) by FUNCT_2:8;

now :: thesis: for u being VECTOR of V st not u in (Carrier l) \ {v} holds
f . u = 0. INT.Ring

let u be VECTOR of V; :: thesis: ( not u in (Carrier l) \ {v} implies f . u = 0. INT.Ring )
assume not u in (Carrier l) \ {v} ; :: thesis: f . u = 0. INT.Ring
then ( not u in Carrier l or u in {v} ) by XBOOLE_0:def 5;
then ( ( l . u = 0. INT.Ring & u <> v ) or u = v ) by TARSKI:def 1;
hence f . u = 0. INT.Ring by A42, A43; :: thesis: verum

end;

then reconsider f = f as Linear_Combination of V by VECTSP_6:def 1;
Carrier f c= B

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Carrier f or x in B )
A44: Carrier l c= B \/ {v} by VECTSP_6:def 4;
assume x in Carrier f ; :: thesis: x in B
then consider u being VECTOR of V such that
A45: u = x and
A46: f . u <> 0. INT.Ring ;
f . u = l . u by A42, A43, A46;
then u in Carrier l by A46;
then ( u in B or u in {v} ) by A44, XBOOLE_0:def 3;
hence x in B by A42, A45, A46, TARSKI:def 1; :: thesis: verum

end;

then reconsider f = f as Linear_Combination of B by VECTSP_6:def 4;
reconsider lv = - (l . v) as Element of INT.Ring ;
consider g being Function of V,INT.Ring such that
A47: g . v = lv and
A48: for u being VECTOR of V st u <> v holds
g . u = H₁(u) from FUNCT_2:sch 6();
reconsider g = g as Element of Funcs ( the carrier of V, the carrier of INT.Ring) by FUNCT_2:8;

now :: thesis: for u being VECTOR of V st not u in {v} holds
g . u = 0. INT.Ring

let u be VECTOR of V; :: thesis: ( not u in {v} implies g . u = 0. INT.Ring )
assume not u in {v} ; :: thesis: g . u = 0. INT.Ring
then u <> v by TARSKI:def 1;
hence g . u = 0. INT.Ring by A48; :: thesis: verum

end;

then reconsider g = g as Linear_Combination of V by VECTSP_6:def 1;
Carrier g c= {v}

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Carrier g or x in {v} )
assume x in Carrier g ; :: thesis: x in {v}
then ex u being VECTOR of V st
( x = u & g . u <> 0. INT.Ring ) ;
then x = v by A48;
hence x in {v} by TARSKI:def 1; :: thesis: verum

end;

then reconsider g = g as Linear_Combination of {v} by VECTSP_6:def 4;
f - g = l

proof

let u be VECTOR of V; :: according to FUNCT_2:def 8 :: thesis: (f - g) . u = l . u

now :: thesis: (f - g) . u = l . u

per cases ( v = u or v <> u ) ;

suppose A50: v = u ; :: thesis: (f - g) . u = l . u

thus (f - g) . u = (f . u) - (g . u) by ZMODUL02:39
.= l . u by A42, A47, A50 ; :: thesis: verum

end;

suppose A51: v <> u ; :: thesis: (f - g) . u = l . u

thus (f - g) . u = (f . u) - (g . u) by ZMODUL02:39
.= (l . u) - (g . u) by A43, A51
.= (l . u) - 0 by A48, A51
.= l . u ; :: thesis: verum

end;

end;

end;

hence (f - g) . u = l . u ; :: thesis: verum

end;

then 0. V = (Sum f) - (Sum g) by A41, ZMODUL02:55;
then B2: Sum f = (0. V) + (Sum g) by RLSUB_2:61
.= (- (l . v)) * v by A47, ZMODUL02:21 ;
- (l . v) <> 0 by B1, ZMODUL02:8;
hence Carrier l = {} by A39, B2, ZMODUL02:64; :: thesis: verum

end;

suppose A52: not v in Carrier l ; :: thesis: Carrier l = {}

Carrier l c= B

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Carrier l or x in B )
assume A53: x in Carrier l ; :: thesis: x in B
Carrier l c= B \/ {v} by VECTSP_6:def 4;
then ( x in B or x in {v} ) by A53, XBOOLE_0:def 3;
hence x in B by A52, A53, TARSKI:def 1; :: thesis: verum

end;

then l is Linear_Combination of B by VECTSP_6:def 4;
hence Carrier l = {} by A38, A41; :: thesis: verum

end;

end;

end;

hence Carrier l = {} ; :: thesis: verum

end;

v in {v} by TARSKI:def 1;
then A54: v in B \/ {v} by XBOOLE_0:def 3;
not (1. INT.Ring) * v in Lin B by A39;
then not v in Lin B ;
then A55: not v in B by ZMODUL02:65;
B c= B \/ {v} by XBOOLE_1:7;
then B \/ {v} in Q by A2, A37, A40, XBOOLE_1:1;
hence contradiction by A35, A36, A54, A55, XBOOLE_1:7; :: thesis: verum