let V be RealLinearSpace; :: thesis: for A being Subset of V st Lin A = V holds
ex B being Subset of V st
( B c= A & B is linearly-independent & Lin B = V )

let A be Subset of V; :: thesis: ( Lin A = V implies ex B being Subset of V st
( B c= A & B is linearly-independent & Lin B = V ) )

assume A1: Lin A = V ; :: thesis: ex B being Subset of V st
( B c= A & B is linearly-independent & Lin B = V )

defpred S1[ set ] means ex B being Subset of V st
( B = \$1 & B c= A & 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 & S1[Z] ) ) from
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
Z <> {} and
A4: Z c= Q and
A5: 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
A6: x in X and
A7: X in Z by TARSKI:def 4;
X in bool the carrier of V by A2, A4, A7;
hence x in the carrier of V by A6; :: thesis: verum
end;
then reconsider W = union Z as Subset of V ;
A8: W is linearly-independent
proof
deffunc H1( object ) -> set = { C where C is Subset of V : ( \$1 in C & C in Z ) } ;
let l be Linear_Combination of W; :: according to RLVECT_3:def 1 :: thesis: ( Sum l = 0. V implies Carrier l = {} )
assume that
A9: Sum l = 0. V and
A10: Carrier l <> {} ; :: thesis: contradiction
consider f being Function such that
A11: dom f = Carrier l and
A12: for x being object st x in Carrier l holds
f . x = H1(x) from reconsider M = rng f as non empty set by ;
set F = the Choice_Function of M;
set S = rng the Choice_Function of M;
A13: now :: thesis: not {} in M
assume {} in M ; :: thesis: contradiction
then consider x being object such that
A14: x in dom f and
A15: f . x = {} by FUNCT_1:def 3;
Carrier l c= W by RLVECT_2:def 6;
then consider X being set such that
A16: x in X and
A17: X in Z by ;
reconsider X = X as Subset of V by A2, A4, A17;
X in { C where C is Subset of V : ( x in C & C in Z ) } by ;
hence contradiction by A11, A12, A14, A15; :: thesis: verum
end;
then A18: dom the Choice_Function of M = M by Lm7;
then dom the Choice_Function of M is finite by ;
then A19: rng the Choice_Function of M is finite by FINSET_1:8;
A20: 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
A21: x in dom the Choice_Function of M and
A22: the Choice_Function of M . x = X by FUNCT_1:def 3;
consider y being object such that
A23: ( y in dom f & f . y = x ) by ;
A24: x = { C where C is Subset of V : ( y in C & C in Z ) } by ;
reconsider x = x as set by TARSKI:1;
X in x by ;
then ex C being Subset of V st
( C = X & y in C & C in Z ) by A24;
hence X in Z ; :: thesis: verum
end;
A25: 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 A20;
then X,Y are_c=-comparable by ;
hence ( X c= Y or Y c= X ) ; :: thesis: verum
end;
rng the Choice_Function of M <> {} by ;
then union (rng the Choice_Function of M) in rng the Choice_Function of M by ;
then union (rng the Choice_Function of M) in Z by A20;
then consider B being Subset of V such that
A26: B = union (rng the Choice_Function of M) and
B c= A and
A27: B is linearly-independent by A2, A4;
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 A28: x in Carrier l ; :: thesis: x in union (rng the Choice_Function of M)
then A29: f . x = { C where C is Subset of V : ( x in C & C in Z ) } by A12;
A30: f . x in M by ;
then the Choice_Function of M . (f . x) in f . x by ;
then A31: ex C being Subset of V st
( the Choice_Function of M . (f . x) = C & x in C & C in Z ) by A29;
the Choice_Function of M . (f . x) in rng the Choice_Function of M by ;
hence x in union (rng the Choice_Function of M) by ; :: thesis: verum
end;
then l is Linear_Combination of B by ;
hence contradiction by A9, A10, A27; :: thesis: verum
end;
W c= A
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in W or x in A )
assume x in W ; :: thesis: x in A
then consider X being set such that
A32: x in X and
A33: X in Z by TARSKI:def 4;
ex B being Subset of V st
( B = X & B c= A & B is linearly-independent ) by A2, A4, A33;
hence x in A by A32; :: thesis: verum
end;
hence union Z in Q by A2, A8; :: thesis: verum
end;
( {} the carrier of V c= A & {} the carrier of V is linearly-independent ) by Th7;
then Q <> {} by 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 ;
consider B being Subset of V such that
A36: B = X and
A37: B c= A and
A38: B is linearly-independent by ;
take B ; :: thesis: ( B c= A & B is linearly-independent & Lin B = V )
thus ( B c= A & B is linearly-independent ) by ; :: thesis: Lin B = V
assume A39: Lin B <> V ; :: thesis: contradiction
now :: thesis: ex v being VECTOR of V st
( v in A & not v in Lin B )
assume A40: for v being VECTOR of V st v in A holds
v in Lin B ; :: thesis: contradiction
now :: thesis: for v being VECTOR of V st v in Lin A holds
v in Lin B
reconsider F = the carrier of (Lin B) as Subset of V by RLSUB_1:def 2;
let v be VECTOR of V; :: thesis: ( v in Lin A implies v in Lin B )
assume v in Lin A ; :: thesis: v in Lin B
then consider l being Linear_Combination of A such that
A41: v = Sum l by Th14;
Carrier l c= the carrier of (Lin B)
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Carrier l or x in the carrier of (Lin B) )
assume A42: x in Carrier l ; :: thesis: x in the carrier of (Lin B)
then reconsider a = x as VECTOR of V ;
Carrier l c= A by RLVECT_2:def 6;
then a in Lin B by ;
hence x in the carrier of (Lin B) by STRUCT_0:def 5; :: thesis: verum
end;
then reconsider l = l as Linear_Combination of F by RLVECT_2:def 6;
Sum l = v by A41;
then v in Lin F by Th14;
hence v in Lin B by Th18; :: thesis: verum
end;
then Lin A is Subspace of Lin B by RLSUB_1:29;
hence contradiction by A1, A39, RLSUB_1:26; :: thesis: verum
end;
then consider v being VECTOR of V such that
A43: v in A and
A44: not v in Lin B ;
A45: B \/ {v} is linearly-independent
proof
let l be Linear_Combination of B \/ {v}; :: according to RLVECT_3:def 1 :: thesis: ( Sum l = 0. V implies Carrier l = {} )
assume A46: Sum l = 0. V ; :: thesis:
now :: thesis:
per cases ( v in Carrier l or not v in Carrier l ) ;
suppose v in Carrier l ; :: thesis:
then A47: - (l . v) <> 0 by RLVECT_2:19;
deffunc H1( VECTOR of V) -> Element of REAL = In (0,REAL);
deffunc H2( VECTOR of V) -> Element of REAL = l . \$1;
consider f being Function of the carrier of V,REAL such that
A48: f . v = In (0,REAL) and
A49: for u being VECTOR of V st u <> v holds
f . u = H2(u) from reconsider f = f as Element of Funcs ( the carrier of V,REAL) by FUNCT_2:8;
now :: thesis: for u being VECTOR of V st not u in () \ {v} holds
f . u = 0
let u be VECTOR of V; :: thesis: ( not u in () \ {v} implies f . u = 0 )
assume not u in () \ {v} ; :: thesis: f . u = 0
then ( not u in Carrier l or u in {v} ) by XBOOLE_0:def 5;
then ( ( l . u = 0 & u <> v ) or u = v ) by TARSKI:def 1;
hence f . u = 0 by ; :: thesis: verum
end;
then reconsider f = f as Linear_Combination of V by RLVECT_2:def 3;
Carrier f c= B
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Carrier f or x in B )
A50: Carrier l c= B \/ {v} by RLVECT_2:def 6;
assume x in Carrier f ; :: thesis: x in B
then consider u being VECTOR of V such that
A51: u = x and
A52: f . u <> 0 ;
f . u = l . u by ;
then u in Carrier l by A52;
then ( u in B or u in {v} ) by ;
hence x in B by ; :: thesis: verum
end;
then reconsider f = f as Linear_Combination of B by RLVECT_2:def 6;
consider g being Function of the carrier of V,REAL such that
A53: g . v = - (l . v) and
A54: for u being VECTOR of V st u <> v holds
g . u = H1(u) from reconsider g = g as Element of Funcs ( the carrier of V,REAL) by FUNCT_2:8;
now :: thesis: for u being VECTOR of V st not u in {v} holds
g . u = 0
let u be VECTOR of V; :: thesis: ( not u in {v} implies g . u = 0 )
assume not u in {v} ; :: thesis: g . u = 0
then u <> v by TARSKI:def 1;
hence g . u = 0 by A54; :: thesis: verum
end;
then reconsider g = g as Linear_Combination of V by RLVECT_2:def 3;
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 ) ;
then x = v by A54;
hence x in {v} by TARSKI:def 1; :: thesis: verum
end;
then reconsider g = g as Linear_Combination of {v} by RLVECT_2:def 6;
A55: Sum g = (- (l . v)) * v by ;
f - g = l
proof
let u be VECTOR of V; :: according to RLVECT_2:def 9 :: thesis: (f - g) . u = l . u
now :: thesis: (f - g) . u = l . u
per cases ( v = u or v <> u ) ;
suppose A56: v = u ; :: thesis: (f - g) . u = l . u
thus (f - g) . u = (f . u) - (g . u) by RLVECT_2:54
.= l . u by ; :: thesis: verum
end;
suppose A57: v <> u ; :: thesis: (f - g) . u = l . u
thus (f - g) . u = (f . u) - (g . u) by RLVECT_2:54
.= (l . u) - (g . u) by
.= (l . u) - 0 by
.= l . u ; :: thesis: verum
end;
end;
end;
hence (f - g) . u = l . u ; :: thesis: verum
end;
then 0. V = (Sum f) - (Sum g) by ;
then Sum f = (0. V) + (Sum g) by RLSUB_2:61
.= (- (l . v)) * v by A55 ;
then A58: (- (l . v)) * v in Lin B by Th14;
((- (l . v)) ") * ((- (l . v)) * v) = (((- (l . v)) ") * (- (l . v))) * v by RLVECT_1:def 7
.= 1 * v by
.= v by RLVECT_1:def 8 ;
hence Carrier l = {} by ; :: thesis: verum
end;
suppose A59: not v in Carrier l ; :: thesis:
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 A60: x in Carrier l ; :: thesis: x in B
Carrier l c= B \/ {v} by RLVECT_2:def 6;
then ( x in B or x in {v} ) by ;
hence x in B by ; :: thesis: verum
end;
then l is Linear_Combination of B by RLVECT_2:def 6;
hence Carrier l = {} by ; :: thesis: verum
end;
end;
end;
hence Carrier l = {} ; :: thesis: verum
end;
{v} c= A by ;
then B \/ {v} c= A by ;
then A61: B \/ {v} in Q by ;
v in {v} by TARSKI:def 1;
then A62: v in B \/ {v} by XBOOLE_0:def 3;
not v in B by ;
hence contradiction by A35, A36, A62, A61, XBOOLE_1:7; :: thesis: verum