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 ;

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 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

( i in dom p & Sum L = p . i ) } as Subset of V by XBOOLE_1:1;

for v being VECTOR of V holds

( v in (Omega). V iff v in Lin C )

then A10: UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #) = Lin C by RUSUB_1:def 3;

A11: B is linearly-independent by RUSUB_3:def 2;

then C is linearly-independent by A3, RLVECT_3:5;

then A12: C is Basis of V by A10, RUSUB_3:def 2;

B c= C

defpred S_{1}[ set , object ] means ex L being Linear_Combination of B st

( $2 = Carrier L & Sum L = p . $1 );

A14: for i being Nat st i in Seg (len p) holds

ex x being object st S_{1}[i,x]

( dom q = Seg (len p) & ( for i being Nat st i in Seg (len p) holds

S_{1}[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_{1}[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_{1}[i,y1] & S_{1}[i,y2] holds

y1 = y2

( 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

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 ;

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 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

then reconsider C = union { (Carrier L) where L is Linear_Combination of B : ex i being Element of NAT st
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 RLVECT_2:def 6;

hence x in B by A4; :: thesis: verum

end;( 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 RLVECT_2:def 6;

hence x in B by A4; :: thesis: verum

( i in dom p & Sum L = p . i ) } as Subset of V by XBOOLE_1:1;

for v being VECTOR of V holds

( v in (Omega). V iff v in Lin C )

proof

then
(Omega). V = Lin C
by RUSUB_1:25;
let v be VECTOR of V; :: thesis: ( v in (Omega). V iff v in Lin C )

v in the carrier of UNITSTR(# the carrier of V, the ZeroF 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 ; :: thesis: verum

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

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

v in UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #) ;

then v in Lin A by A1, RUSUB_3:def 2;

then consider LA being Linear_Combination of A such that

A6: v = Sum LA by RUSUB_3:1;

Carrier LA c= the carrier of (Lin C)

hence v in Lin C by A6, RUSUB_3:1; :: thesis: verum

end;v in UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #) ;

then v in Lin A by A1, RUSUB_3:def 2;

then consider LA being Linear_Combination of A such that

A6: v = Sum LA by RUSUB_3:1;

Carrier LA c= the carrier of (Lin C)

proof

then
ex LC being Linear_Combination of C st Sum LA = Sum LC
by RUSUB_3:17;
let w be object ; :: according to TARSKI:def 3 :: thesis: ( not w in Carrier LA or w in the carrier of (Lin C) )

assume A7: 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 RUSUB_3:21;

then consider LB being Linear_Combination of B such that

A8: w = Sum LB by RUSUB_3:1;

Carrier LA c= A by RLVECT_2:def 6;

then ex i being object st

( i in dom p & w = p . i ) by A2, A7, FUNCT_1:def 3;

then A9: 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 A8;

Carrier LB c= C by A9, TARSKI:def 4;

then LB is Linear_Combination of C by RLVECT_2:def 6;

then w in Lin C by A8, RUSUB_3:1;

hence w in the carrier of (Lin C) ; :: thesis: verum

end;assume A7: 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 RUSUB_3:21;

then consider LB being Linear_Combination of B such that

A8: w = Sum LB by RUSUB_3:1;

Carrier LA c= A by RLVECT_2:def 6;

then ex i being object st

( i in dom p & w = p . i ) by A2, A7, FUNCT_1:def 3;

then A9: 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 A8;

Carrier LB c= C by A9, TARSKI:def 4;

then LB is Linear_Combination of C by RLVECT_2:def 6;

then w in Lin C by A8, RUSUB_3:1;

hence w in the carrier of (Lin C) ; :: thesis: verum

hence v in Lin C by A6, RUSUB_3:1; :: thesis: verum

v in the carrier of UNITSTR(# the carrier of V, the ZeroF 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 ; :: thesis: verum

then A10: UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #) = Lin C by RUSUB_1:def 3;

A11: B is linearly-independent by RUSUB_3:def 2;

then C is linearly-independent by A3, RLVECT_3:5;

then A12: C is Basis of V by A10, RUSUB_3:def 2;

B c= C

proof

then A13:
B = C
by A3;
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, RUSUB_3:26, XBOOLE_1:79; :: thesis: verum

end;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, RUSUB_3:26, XBOOLE_1:79; :: thesis: verum

defpred S

( $2 = Carrier L & Sum L = p . $1 );

A14: for i being Nat st i in Seg (len p) holds

ex x being object st S

proof

ex q being FinSequence st
let i be Nat; :: thesis: ( i in Seg (len p) implies ex x being object st S_{1}[i,x] )

assume i in Seg (len p) ; :: thesis: ex x being object st S_{1}[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 RUSUB_3:21;

then consider L being Linear_Combination of B such that

A15: p . i = Sum L by RUSUB_3:1;

S_{1}[i, Carrier L]
by A15;

hence ex x being object st S_{1}[i,x]
; :: thesis: verum

end;assume i in Seg (len p) ; :: thesis: ex x being object st S

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 RUSUB_3:21;

then consider L being Linear_Combination of B such that

A15: p . i = Sum L by RUSUB_3:1;

S

hence ex x being object st S

( dom q = Seg (len p) & ( for i being Nat st i in Seg (len p) holds

S

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

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

y1 = y2

proof

let i be Nat; :: thesis: for y1, y2 being set st i in Seg (len p) & S_{1}[i,y1] & S_{1}[i,y2] holds

y1 = y2

let y1, y2 be set ; :: thesis: ( i in Seg (len p) & S_{1}[i,y1] & S_{1}[i,y2] implies y1 = y2 )

assume that

i in Seg (len p) and

A20: S_{1}[i,y1]
and

A21: S_{1}[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 RLVECT_2:def 6;

hence y1 = y2 by A11, A22, A23, RLVECT_5:1; :: thesis: verum

end;y1 = y2

let y1, y2 be set ; :: thesis: ( i in Seg (len p) & S

assume that

i in Seg (len p) and

A20: S

A21: S

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 RLVECT_2:def 6;

hence y1 = y2 by A11, A22, A23, RLVECT_5:1; :: thesis: verum

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

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 ) } 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_{1}[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;( 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

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

( 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

hence
B is finite
by A13, A28, FINSET_1:7; :: thesis: verum
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;( 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