let V be RealUnitarySpace; :: 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 Def1;
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 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 set ; :: 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;
consider L being Linear_Combination of B such that
A6: R = Carrier L and
ex i being Element of NAT st
( i in dom p & Sum L = p . i ) by A5;
R c= B by A6, RLVECT_2:def 8;
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;
A7: B is linearly-independent by RUSUB_3:def 2;
then A8: C is linearly-independent by A3, RLVECT_3:6;
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 UNITSTR(# the carrier of V,the U2 of V,the addF of V,the Mult of V,the scalar of V #) by RUSUB_1:def 3;
then v in Lin A by A1, RUSUB_3:def 2;
then consider LA being Linear_Combination of A such that
A9: v = Sum LA by RUSUB_3:1;
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 RLVECT_2:def 8;
reconsider w' = w as VECTOR of V by A10;
w' in Lin B by RUSUB_3:21;
then consider LB being Linear_Combination of B such that
A12: w = Sum LB by RUSUB_3:1;
ex i being set st
( i in dom p & w = p . i ) by A2, A11, FUNCT_1:def 5;
then A13: 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 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 A13, TARSKI:def 4; :: thesis: verum

end;

then LB is Linear_Combination of C by RLVECT_2:def 8;
then w in Lin C by A12, RUSUB_3:1;
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
A14: Sum LA = Sum LC by RUSUB_3:17;
thus v in Lin C by A9, A14, RUSUB_3:1; :: thesis: verum

end;

assume v in Lin C ; :: thesis: v in (Omega). V
v in the carrier of UNITSTR(# the carrier of V,the U2 of V,the addF of V,the Mult of V,the scalar of V #) ;
then v in the carrier of ((Omega). V) by RUSUB_1:def 3;
hence v in (Omega). V by STRUCT_0:def 5; :: thesis: verum

end;

then (Omega). V = Lin C by RUSUB_1:25;
then UNITSTR(# the carrier of V,the U2 of V,the addF of V,the Mult of V,the scalar of V #) = Lin C by RUSUB_1:def 3;
then A15: C is Basis of V by A8, RUSUB_3:def 2;
B c= C

proof

assume not B c= C ; :: thesis: contradiction
then consider v being set such that
A16: v in B and
A17: 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 A16, A17, 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, A15, RUSUB_3:26, XBOOLE_1:79; :: thesis: verum

end;

then A18: 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 );
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 and
A23: Sum L1 = p . i by A20;
consider L2 being Linear_Combination of B such that
A24: y2 = Carrier L2 and
A25: Sum L2 = p . i by A21;
( Carrier L1 c= B & Carrier L2 c= B ) by RLVECT_2:def 8;
hence y1 = y2 by A7, A22, A23, A24, A25, RLVECT_5:1; :: thesis: verum

end;

A26: 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 RUSUB_3:21;
then consider L being Linear_Combination of B such that
A27: p . i = Sum L by RUSUB_3:1;
S₁[i, Carrier L] by A27;
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(A26);
then consider q being FinSequence such that
A28: ( dom q = Seg (len p) & ( for i being Nat st i in Seg (len p) holds
S₁[i,q . i] ) ) ;
A29: dom p = dom q by A28, FINSEQ_1:def 3;

now

let x be set ; :: 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
A35: x = Carrier L and
A36: ex i being Element of NAT st
( i in dom p & Sum L = p . i ) ;
consider i being Element of NAT such that
A37: ( i in dom p & Sum L = p . i ) by A36;
( S₁[i,x] & S₁[i,q . i] ) by A28, A29, A35, A37;
then x = q . i by A19, A28, A29, A37;
hence x in rng q by A29, A37, FUNCT_1:def 5; :: thesis: verum

end;

then { (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 by TARSKI:def 3;
then A38: { (Carrier L) where L is Linear_Combination of B : ex i being Element of 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 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 consider L being Linear_Combination of B such that
A39: R = Carrier L and
ex i being Element of NAT st
( i in dom p & Sum L = p . i ) ;
thus R is finite by A39; :: thesis: verum

end;

hence B is finite by A18, A38, FINSET_1:25; :: thesis: verum