let GF be Field; :: thesis: for V being VectSp of GF st V is finite-dimensional holds
for I being Basis of V holds I is finite
let V be VectSp of GF; :: thesis: ( V is finite-dimensional implies for I being Basis of V holds I is finite )
assume V is finite-dimensional ; :: thesis: for I being Basis of V holds I is finite
then consider A being finite Subset of V such that
A1: A is Basis of V by MATRLIN:def 3;
let B be Basis of V; :: thesis: B is finite
consider p being FinSequence such that
A2: rng p = A by FINSEQ_1:73;
reconsider p = p as FinSequence of the carrier of V by A2, FINSEQ_1:def 4;
set Car = { (Carrier L) where L is Linear_Combination of B : ex i being Nat st
( i in dom p & Sum L = p . i ) } ;
set C = union { (Carrier L) where L is Linear_Combination of B : ex i being Nat st
( i in dom p & Sum L = p . i ) } ;
A3: union { (Carrier L) where L is Linear_Combination of B : ex i being Nat st
( i in dom p & Sum L = p . i ) } c= B

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in union { (Carrier L) where L is Linear_Combination of B : ex i being Nat st
( i in dom p & Sum L = p . i ) } or x in B )
assume x in union { (Carrier L) where L is Linear_Combination of B : ex i being Nat st
( i in dom p & Sum L = p . i ) } ; :: thesis: x in B
then consider R being set such that
A4: x in R and
A5: R in { (Carrier L) where L is Linear_Combination of B : ex i being Nat st
( i in dom p & Sum L = p . i ) } by TARSKI:def 4;
consider L being Linear_Combination of B such that
A6: R = Carrier L and
ex i being Nat st
( i in dom p & Sum L = p . i ) by A5;
R c= B by A6, VECTSP_6:def 7;
hence x in B by A4; :: thesis: verum

end;

then reconsider C = union { (Carrier L) where L is Linear_Combination of B : ex i being Nat st
( i in dom p & Sum L = p . i ) } as Subset of V by XBOOLE_1:1;
A7: B is linearly-independent by VECTSP_7:def 3;
then A8: C is linearly-independent by A3, VECTSP_7:2;
for v being Vector of V holds
( v in (Omega). V iff v in Lin C )

proof

let v be Vector of V; :: thesis: ( v in (Omega). V iff v in Lin C )

hereby :: thesis: ( v in Lin C implies v in (Omega). V )

assume v in (Omega). V ; :: thesis: v in Lin C
then v in VectSpStr(# the carrier of V,the U5 of V,the U2 of V,the lmult of V #) by VECTSP_4:def 4;
then v in Lin A by A1, VECTSP_7:def 3;
then consider LA being Linear_Combination of A such that
A9: v = Sum LA by VECTSP_7:12;
Carrier LA c= the carrier of (Lin C)

proof

let w be set ; :: according to TARSKI:def 3 :: thesis: ( not w in Carrier LA or w in the carrier of (Lin C) )
assume A10: w in Carrier LA ; :: thesis: w in the carrier of (Lin C)
then A11: ( w in Carrier LA & Carrier LA c= A ) by VECTSP_6:def 7;
reconsider w' = w as Vector of V by A10;
w' in Lin B by Th14;
then consider LB being Linear_Combination of B such that
A12: w = Sum LB by VECTSP_7:12;
ex i being Nat st
( i in dom p & w = p . i )

proof

consider i being set such that
A13: i in dom p and
A14: w = p . i by A2, A11, FUNCT_1:def 5;
reconsider i = i as Element of NAT by A13;
take i ; :: thesis: ( i in dom p & w = p . i )
thus ( i in dom p & w = p . i ) by A13, A14; :: thesis: verum

end;

then A15: Carrier LB in { (Carrier L) where L is Linear_Combination of B : ex i being Nat st
( i in dom p & Sum L = p . i ) } by A12;
Carrier LB c= C

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in Carrier LB or x in C )
assume x in Carrier LB ; :: thesis: x in C
hence x in C by A15, TARSKI:def 4; :: thesis: verum

end;

then LB is Linear_Combination of C by VECTSP_6:def 7;
then w in Lin C by A12, VECTSP_7:12;
hence w in the carrier of (Lin C) by STRUCT_0:def 5; :: thesis: verum

end;

then consider LC being Linear_Combination of C such that
A16: Sum LA = Sum LC by Th10;
thus v in Lin C by A9, A16, VECTSP_7:12; :: thesis: verum

end;

assume v in Lin C ; :: thesis: v in (Omega). V
v in the carrier of VectSpStr(# the carrier of V,the U5 of V,the U2 of V,the lmult of V #) ;
then v in the carrier of ((Omega). V) by VECTSP_4:def 4;
hence v in (Omega). V by STRUCT_0:def 5; :: thesis: verum

end;

then (Omega). V = Lin C by VECTSP_4:38;
then VectSpStr(# the carrier of V,the U5 of V,the U2 of V,the lmult of V #) = Lin C by VECTSP_4:def 4;
then A17: C is Basis of V by A8, VECTSP_7:def 3;
B c= C

proof

assume not B c= C ; :: thesis: contradiction
then consider v being set such that
A18: v in B and
A19: not v in C by TARSKI:def 3;
set D = B \ C;
reconsider B = B as Subset of V ;
reconsider D = B \ C as non empty Subset of V by A18, A19, XBOOLE_0:def 5;
C \/ (B \ C) = C \/ B by XBOOLE_1:39
.= B by A3, XBOOLE_1:12 ;
then B = C \/ D ;
hence contradiction by A7, A17, Th19, XBOOLE_1:79; :: thesis: verum

end;

then A20: B = C by A3, XBOOLE_0:def 10;
defpred S₁[ set , set ] means ex L being Linear_Combination of B st
( $2 = Carrier L & Sum L = p . $1 );
A21: for i being Nat
for y1, y2 being set st i in Seg (len p) & S₁[i,y1] & S₁[i,y2] holds
y1 = y2

proof

let i be Nat; :: thesis: for y1, y2 being set st i in Seg (len p) & S₁[i,y1] & S₁[i,y2] holds
y1 = y2
let y1, y2 be set ; :: thesis: ( i in Seg (len p) & S₁[i,y1] & S₁[i,y2] implies y1 = y2 )
assume that
i in Seg (len p) and
A22: S₁[i,y1] and
A23: S₁[i,y2] ; :: thesis: y1 = y2
consider L1 being Linear_Combination of B such that
A24: y1 = Carrier L1 and
A25: Sum L1 = p . i by A22;
consider L2 being Linear_Combination of B such that
A26: y2 = Carrier L2 and
A27: Sum L2 = p . i by A23;
( Carrier L1 c= B & Carrier L2 c= B ) by VECTSP_6:def 7;
hence y1 = y2 by A7, A24, A25, A26, A27, MATRLIN:9; :: thesis: verum

end;

A28: for i being Nat st i in Seg (len p) holds
ex x being set st S₁[i,x]

proof

let i be Nat; :: thesis: ( i in Seg (len p) implies ex x being set st S₁[i,x] )
assume i in Seg (len p) ; :: thesis: ex x being set st S₁[i,x]
then i in dom p by FINSEQ_1:def 3;
then p . i in the carrier of V by FINSEQ_2:13;
then p . i in Lin B by Th14;
then consider L being Linear_Combination of B such that
A29: p . i = Sum L by VECTSP_7:12;
S₁[i, Carrier L] by A29;
hence ex x being set st S₁[i,x] ; :: thesis: verum

end;

ex q being FinSequence st
( dom q = Seg (len p) & ( for i being Nat st i in Seg (len p) holds
S₁[i,q . i] ) ) from FINSEQ_1:sch 1(A28);
then consider q being FinSequence such that
A30: ( dom q = Seg (len p) & ( for i being Nat st i in Seg (len p) holds
S₁[i,q . i] ) ) ;
A31: dom p = dom q by A30, FINSEQ_1:def 3;

now

let x be set ; :: thesis: ( x in { (Carrier L) where L is Linear_Combination of B : ex i being Nat st
( i in dom p & Sum L = p . i ) } implies x in rng q )
assume x in { (Carrier L) where L is Linear_Combination of B : ex i being Nat st
( i in dom p & Sum L = p . i ) } ; :: thesis: x in rng q
then consider L being Linear_Combination of B such that
A37: x = Carrier L and
A38: ex i being Nat st
( i in dom p & Sum L = p . i ) ;
consider i being Nat such that
A39: ( i in dom p & Sum L = p . i ) by A38;
( S₁[i,x] & S₁[i,q . i] ) by A30, A31, A37, A39;
then x = q . i by A21, A30, A31, A39;
hence x in rng q by A31, A39, FUNCT_1:def 5; :: thesis: verum

end;

then { (Carrier L) where L is Linear_Combination of B : ex i being Nat st
( i in dom p & Sum L = p . i ) } c= rng q by TARSKI:def 3;
then A40: { (Carrier L) where L is Linear_Combination of B : ex i being Nat st
( i in dom p & Sum L = p . i ) } is finite ;
for R being set st R in { (Carrier L) where L is Linear_Combination of B : ex i being Nat st
( i in dom p & Sum L = p . i ) } holds
R is finite

proof

let R be set ; :: thesis: ( R in { (Carrier L) where L is Linear_Combination of B : ex i being Nat st
( i in dom p & Sum L = p . i ) } implies R is finite )
assume R in { (Carrier L) where L is Linear_Combination of B : ex i being Nat st
( i in dom p & Sum L = p . i ) } ; :: thesis: R is finite
then consider L being Linear_Combination of B such that
A41: R = Carrier L and
ex i being Nat st
( i in dom p & Sum L = p . i ) ;
thus R is finite by A41; :: thesis: verum

end;

hence B is finite by A20, A40, FINSET_1:25; :: thesis: verum