consider A being finite Subset of V such that
A1: A is Basis of V by Def3;
let B be Basis of V; :: thesis: B is finite
consider p being FinSequence such that
A2: rng p = A by FINSEQ_1:52;
reconsider p = p as FinSequence of V by A2, FINSEQ_1:def 4;
set Car = { (Carrier L) where L is Linear_Combination of B : ex i being Element of 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 Element of NAT st
( i in dom p & Sum L = p . i ) } ;
A3: union { (Carrier L) where L is Linear_Combination of B : ex i being Element of NAT st
( i in dom p & Sum L = p . i ) } c= B

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in union { (Carrier L) where L is Linear_Combination of B : ex i being Element of 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 Element of 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 Element of NAT st
( i in dom p & Sum L = p . i ) } by TARSKI:def 4;
ex L being Linear_Combination of B st
( R = Carrier L & ex i being Element of NAT st
( i in dom p & Sum L = p . i ) ) by A5;
then R c= B by VECTSP_6:def 4;
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 Element of NAT st
( i in dom p & Sum L = p . i ) } as Subset of V by XBOOLE_1:1;
A6: 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 Lin A by A1, VECTSP_7:def 3;
then consider LA being Linear_Combination of A such that
A7: v = Sum LA by ZMODUL02:64;
Carrier LA c= the carrier of (Lin C)

proof

let w be object ; :: according to TARSKI:def 3 :: thesis: ( not w in Carrier LA or w in the carrier of (Lin C) )
assume A8: w in Carrier LA ; :: thesis: w in the carrier of (Lin C)
then reconsider w9 = w as Vector of V ;
w9 in Lin B by Th14;
then consider LB being Linear_Combination of B such that
A9: w = Sum LB by ZMODUL02:64;
Carrier LA c= A by VECTSP_6:def 4;
then ex i being object st
( i in dom p & w = p . i ) by A2, A8, FUNCT_1:def 3;
then A10: Carrier LB in { (Carrier L) where L is Linear_Combination of B : ex i being Element of NAT st
( i in dom p & Sum L = p . i ) } by A9;
Carrier LB c= C by A10, TARSKI:def 4;
then LB is Linear_Combination of C by VECTSP_6:def 4;
hence w in the carrier of (Lin C) by A9, STRUCT_0:def 5, ZMODUL02:64; :: thesis: verum

end;

then ex LC being Linear_Combination of C st Sum LA = Sum LC by Th10;
hence v in Lin C by A7, ZMODUL02:64; :: thesis: verum

end;

assume v in Lin C ; :: thesis: v in (Omega). V
thus v in (Omega). V ; :: thesis: verum

end;

A11: B is linearly-independent by VECTSP_7:def 3;
C is linearly-independent by A3, VECTSP_7:def 3, ZMODUL02:56;
then A12: C is Basis of V by A6, VECTSP_7:def 3, ZMODUL01:46;
B c= C

proof

set D = B \ C;
assume not B c= C ; :: thesis: contradiction
then ex v being object st
( v in B & not v in C ) ;
then reconsider D = B \ C as non empty Subset of V by XBOOLE_0:def 5;
reconsider B = B as Subset of V ;
C \/ (B \ C) = C \/ B by XBOOLE_1:39
.= B by A3, XBOOLE_1:12 ;
then B = C \/ D ;
hence contradiction by A11, A12, Th18, XBOOLE_1:79; :: thesis: verum

end;

then A13: B = C by A3, XBOOLE_0:def 10;
defpred S₁[ set , object ] means ex L being Linear_Combination of B st
( c₂ = Carrier L & Sum L = p . V );
A14: for i being Nat st i in Seg (len p) holds
ex x being object st S₁[i,x]

proof

let i be Nat; :: thesis: ( i in Seg (len p) implies ex x being object st S₁[i,x] )
assume i in Seg (len p) ; :: thesis: ex x being object 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:11;
then p . i in Lin B by Th14;
then consider L being Linear_Combination of B such that
A15: p . i = Sum L by ZMODUL02:64;
S₁[i, Carrier L] by A15;
hence ex x being object 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(A14);
then consider q being FinSequence such that
A16: dom q = Seg (len p) and
A17: for i being Nat st i in Seg (len p) holds
S₁[i,q . i] ;
A18: dom p = dom q by A16, FINSEQ_1:def 3;
A19: 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
A20: S₁[i,y1] and
A21: S₁[i,y2] ; :: thesis: y1 = y2
consider L1 being Linear_Combination of B such that
A22: ( y1 = Carrier L1 & Sum L1 = p . i ) by A20;
consider L2 being Linear_Combination of B such that
A23: ( y2 = Carrier L2 & Sum L2 = p . i ) by A21;
( Carrier L1 c= B & Carrier L2 c= B ) by VECTSP_6:def 4;
hence y1 = y2 by A22, A23, VECTSP_7:def 3, Th3; :: thesis: verum

end;

now :: thesis: for x being object st x in { (Carrier L) where L is Linear_Combination of B : ex i being Element of NAT st
( i in dom p & Sum L = p . i ) } holds
x in rng q

let x be object ; :: thesis: ( x in { (Carrier L) where L is Linear_Combination of B : ex i being Element of 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 Element of 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
A24: x = Carrier L and
A25: ex i being Element of NAT st
( i in dom p & Sum L = p . i ) ;
consider i being Element of NAT such that
A26: i in dom p and
A27: Sum L = p . i by A25;
S₁[i,q . i] by A16, A17, A18, A26;
then x = q . i by A19, A16, A18, A24, A26, A27;
hence x in rng q by A18, A26, FUNCT_1:def 3; :: thesis: verum

end;

then A28: { (Carrier L) where L is Linear_Combination of B : ex i being Element of NAT st
( i in dom p & Sum L = p . i ) } c= rng q ;
for R being set st R in { (Carrier L) where L is Linear_Combination of B : ex i being Element of 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 Element of 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 Element of NAT st
( i in dom p & Sum L = p . i ) } ; :: thesis: R is finite
then ex L being Linear_Combination of B st
( R = Carrier L & ex i being Element of NAT st
( i in dom p & Sum L = p . i ) ) ;
hence R is finite ; :: thesis: verum

end;

hence B is finite by A13, A28, FINSET_1:7; :: thesis: verum