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
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 RLVECT_2:def 6;
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;
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
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
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;
then ex LC being Linear_Combination of C st Sum LA = Sum LC by RUSUB_3:17;
hence v in Lin C by A6, 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 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;
then (Omega). V = Lin C by RUSUB_1:25;
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
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;
then A13: B = C by A3;
defpred S1[ 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 S1[i,x]
proof
let i be Nat; :: thesis: ( i in Seg (len p) implies ex x being object st S1[i,x] )
assume i in Seg (len p) ; :: thesis: ex x being object st S1[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;
S1[i, Carrier L] by A15;
hence ex x being object st S1[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
S1[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
S1[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) & S1[i,y1] & S1[i,y2] holds
y1 = y2
proof
let i be Nat; :: thesis: for y1, y2 being set st i in Seg (len p) & S1[i,y1] & S1[i,y2] holds
y1 = y2
let y1, y2 be set ; :: thesis: ( i in Seg (len p) & S1[i,y1] & S1[i,y2] implies y1 = y2 )
assume that
i in Seg (len p) and
A20: S1[i,y1] and
A21: S1[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;
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;
S1[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