:: The Real Vector Spaces of Finite Sequences Are Finite Dimensional
:: by Yatsuka Nakamura , Artur Korni{\l}owicz , Nagato Oya and Yasunari Shidama
::
:: Received September 23, 2008
:: Copyright (c) 2008-2012 Association of Mizar Users


begin

theorem :: EUCLID_7:1
for f, g being Function holds dom (f * g) = (dom g) /\ (g " (dom f))
proof end;

theorem Th2: :: EUCLID_7:2
for R being Relation
for Y being set st rng R c= Y holds
R " Y = dom R
proof end;

Lm1: for X being set
for Y being non empty set
for f being Function of X,Y st f is bijective holds
card X = card Y

by EULER_1:11;

theorem :: EUCLID_7:3
for z being set holds <*z*> * <*1*> = <*z*>
proof end;

theorem :: EUCLID_7:4
for x being Element of REAL 0 holds x = <*> REAL ;

theorem Th5: :: EUCLID_7:5
for n being Nat
for a, b, c being Element of REAL n holds ((a - b) + c) + b = a + c
proof end;

registration
let f1, f2 be FinSequence;
cluster <:f1,f2:> -> FinSequence-like ;
coherence
<:f1,f2:> is FinSequence-like
proof end;
end;

definition
let D be set ;
let f1, f2 be FinSequence of D;
:: original: <:
redefine func <:f1,f2:> -> FinSequence of [:D,D:];
coherence
<:f1,f2:> is FinSequence of [:D,D:]
proof end;
end;

Lm2: for n, m being Nat st n < m holds
ex k being Nat st m = (n + 1) + k

proof end;

definition
let h be real-valued FinSequence;
redefine attr h is increasing means :Def1: :: EUCLID_7:def 1
for i being Nat st 1 <= i & i < len h holds
h . i < h . (i + 1);
compatibility
( h is increasing iff for i being Nat st 1 <= i & i < len h holds
h . i < h . (i + 1) )
proof end;
end;

:: deftheorem Def1 defines increasing EUCLID_7:def 1 :
for h being real-valued FinSequence holds
( h is increasing iff for i being Nat st 1 <= i & i < len h holds
h . i < h . (i + 1) );

theorem Th6: :: EUCLID_7:6
for h being real-valued FinSequence st h is increasing holds
for i, j being Nat st i < j & 1 <= i & j <= len h holds
h . i < h . j
proof end;

theorem Th7: :: EUCLID_7:7
for h being real-valued FinSequence st h is increasing holds
for i, j being Nat st i <= j & 1 <= i & j <= len h holds
h . i <= h . j
proof end;

theorem Th8: :: EUCLID_7:8
for h being natural-valued FinSequence st h is increasing holds
for i being Nat st i <= len h & 1 <= h . 1 holds
i <= h . i
proof end;

theorem Th9: :: EUCLID_7:9
for V being RealLinearSpace
for X being Subspace of V st V is strict & X is strict & the carrier of X = the carrier of V holds
X = V
proof end;

definition
let D be set ;
let F be FinSequence of D;
let h be Permutation of (dom F);
func F (*) h -> FinSequence of D equals :: EUCLID_7:def 2
F * h;
coherence
F * h is FinSequence of D
proof end;
end;

:: deftheorem defines (*) EUCLID_7:def 2 :
for D being set
for F being FinSequence of D
for h being Permutation of (dom F) holds F (*) h = F * h;

theorem Th10: :: EUCLID_7:10
for i, j being Nat
for D being non empty set
for f being FinSequence of D st 1 <= i & i <= len f & 1 <= j & j <= len f holds
( (Swap (f,i,j)) . i = f . j & (Swap (f,i,j)) . j = f . i )
proof end;

theorem Th11: :: EUCLID_7:11
{} is Permutation of {}
proof end;

theorem :: EUCLID_7:12
<*1*> is Permutation of {1}
proof end;

theorem Th13: :: EUCLID_7:13
for h being FinSequence of REAL holds
( h is one-to-one iff sort_a h is one-to-one )
proof end;

theorem Th14: :: EUCLID_7:14
for h being FinSequence of NAT st h is one-to-one holds
ex h3 being Permutation of (dom h) ex h2 being FinSequence of NAT st
( h2 = h * h3 & h2 is increasing & dom h = dom h2 & rng h = rng h2 )
proof end;

begin

definition
let B0 be set ;
attr B0 is R-orthogonal means :Def3: :: EUCLID_7:def 3
for x, y being real-valued FinSequence st x in B0 & y in B0 & x <> y holds
|(x,y)| = 0 ;
end;

:: deftheorem Def3 defines R-orthogonal EUCLID_7:def 3 :
for B0 being set holds
( B0 is R-orthogonal iff for x, y being real-valued FinSequence st x in B0 & y in B0 & x <> y holds
|(x,y)| = 0 );

registration
cluster empty -> R-orthogonal for set ;
coherence
for b1 being set st b1 is empty holds
b1 is R-orthogonal
proof end;
end;

theorem :: EUCLID_7:15
for B0 being set holds
( B0 is R-orthogonal iff for x, y being real-valued FinSequence st x in B0 & y in B0 & x <> y holds
x,y are_orthogonal )
proof end;

definition
let B0 be set ;
attr B0 is R-normal means :Def4: :: EUCLID_7:def 4
for x being real-valued FinSequence st x in B0 holds
|.x.| = 1;
end;

:: deftheorem Def4 defines R-normal EUCLID_7:def 4 :
for B0 being set holds
( B0 is R-normal iff for x being real-valued FinSequence st x in B0 holds
|.x.| = 1 );

registration
cluster empty -> R-normal for set ;
coherence
for b1 being set st b1 is empty holds
b1 is R-normal
proof end;
end;

registration
cluster R-normal for set ;
existence
ex b1 being set st b1 is R-normal
proof end;
end;

registration
let B0, B1 be R-normal set ;
cluster B0 \/ B1 -> R-normal ;
coherence
B0 \/ B1 is R-normal
proof end;
end;

theorem Th16: :: EUCLID_7:16
for f being real-valued FinSequence st |.f.| = 1 holds
{f} is R-normal
proof end;

theorem Th17: :: EUCLID_7:17
for B0 being set
for x0 being real-valued FinSequence st B0 is R-normal & |.x0.| = 1 holds
B0 \/ {x0} is R-normal
proof end;

definition
let B0 be set ;
attr B0 is R-orthonormal means :Def5: :: EUCLID_7:def 5
( B0 is R-orthogonal & B0 is R-normal );
end;

:: deftheorem Def5 defines R-orthonormal EUCLID_7:def 5 :
for B0 being set holds
( B0 is R-orthonormal iff ( B0 is R-orthogonal & B0 is R-normal ) );

registration
cluster R-orthonormal -> R-orthogonal R-normal for set ;
coherence
for b1 being set st b1 is R-orthonormal holds
( b1 is R-orthogonal & b1 is R-normal )
by Def5;
cluster R-orthogonal R-normal -> R-orthonormal for set ;
coherence
for b1 being set st b1 is R-orthogonal & b1 is R-normal holds
b1 is R-orthonormal
by Def5;
end;

registration
cluster {<*1*>} -> R-orthonormal ;
coherence
{<*1*>} is R-orthonormal
proof end;
end;

registration
cluster non empty R-orthonormal for set ;
existence
ex b1 being set st
( b1 is R-orthonormal & not b1 is empty )
proof end;
end;

registration
let n be Nat;
cluster functional FinSequence-membered R-orthonormal for Element of bool (REAL n);
existence
ex b1 being Subset of (REAL n) st b1 is R-orthonormal
proof end;
end;

definition
let n be Nat;
let B0 be Subset of (REAL n);
attr B0 is complete means :Def6: :: EUCLID_7:def 6
for B being R-orthonormal Subset of (REAL n) st B0 c= B holds
B = B0;
end;

:: deftheorem Def6 defines complete EUCLID_7:def 6 :
for n being Nat
for B0 being Subset of (REAL n) holds
( B0 is complete iff for B being R-orthonormal Subset of (REAL n) st B0 c= B holds
B = B0 );

definition
let n be Nat;
let B0 be Subset of (REAL n);
attr B0 is orthogonal_basis means :Def7: :: EUCLID_7:def 7
( B0 is R-orthonormal & B0 is complete );
end;

:: deftheorem Def7 defines orthogonal_basis EUCLID_7:def 7 :
for n being Nat
for B0 being Subset of (REAL n) holds
( B0 is orthogonal_basis iff ( B0 is R-orthonormal & B0 is complete ) );

registration
let n be Nat;
cluster orthogonal_basis -> R-orthonormal complete for Element of bool (REAL n);
coherence
for b1 being Subset of (REAL n) st b1 is orthogonal_basis holds
( b1 is R-orthonormal & b1 is complete )
by Def7;
cluster R-orthonormal complete -> orthogonal_basis for Element of bool (REAL n);
coherence
for b1 being Subset of (REAL n) st b1 is R-orthonormal & b1 is complete holds
b1 is orthogonal_basis
by Def7;
end;

theorem Th18: :: EUCLID_7:18
for B0 being Subset of (REAL 0) st B0 is orthogonal_basis holds
B0 = {}
proof end;

theorem :: EUCLID_7:19
for n being Nat
for B0 being Subset of (REAL n)
for y being Element of REAL n st B0 is orthogonal_basis & ( for x being Element of REAL n st x in B0 holds
|(x,y)| = 0 ) holds
y = 0* n
proof end;

begin

definition
let n be Nat;
let X be Subset of (REAL n);
attr X is linear_manifold means :Def8: :: EUCLID_7:def 8
for x, y being Element of REAL n
for a, b being Element of REAL st x in X & y in X holds
(a * x) + (b * y) in X;
end;

:: deftheorem Def8 defines linear_manifold EUCLID_7:def 8 :
for n being Nat
for X being Subset of (REAL n) holds
( X is linear_manifold iff for x, y being Element of REAL n
for a, b being Element of REAL st x in X & y in X holds
(a * x) + (b * y) in X );

registration
let n be Nat;
cluster [#] (REAL n) -> linear_manifold ;
coherence
[#] (REAL n) is linear_manifold
proof end;
end;

theorem Th20: :: EUCLID_7:20
for n being Nat holds {(0* n)} is linear_manifold
proof end;

registration
let n be Nat;
cluster {(0* n)} -> linear_manifold for Subset of (REAL n);
coherence
for b1 being Subset of (REAL n) st b1 = {(0* n)} holds
b1 is linear_manifold
by Th20;
end;

definition
let n be Nat;
let X be Subset of (REAL n);
func L_Span X -> Subset of (REAL n) equals :: EUCLID_7:def 9
meet { Y where Y is Subset of (REAL n) : ( Y is linear_manifold & X c= Y ) } ;
correctness
coherence
meet { Y where Y is Subset of (REAL n) : ( Y is linear_manifold & X c= Y ) } is Subset of (REAL n)
;
proof end;
end;

:: deftheorem defines L_Span EUCLID_7:def 9 :
for n being Nat
for X being Subset of (REAL n) holds L_Span X = meet { Y where Y is Subset of (REAL n) : ( Y is linear_manifold & X c= Y ) } ;

registration
let n be Nat;
let X be Subset of (REAL n);
cluster L_Span X -> linear_manifold ;
coherence
L_Span X is linear_manifold
proof end;
end;

definition
let n be Nat;
let f be FinSequence of REAL n;
func accum f -> FinSequence of REAL n means :Def10: :: EUCLID_7:def 10
( len f = len it & f . 1 = it . 1 & ( for i being Nat st 1 <= i & i < len f holds
it . (i + 1) = (it /. i) + (f /. (i + 1)) ) );
existence
ex b1 being FinSequence of REAL n st
( len f = len b1 & f . 1 = b1 . 1 & ( for i being Nat st 1 <= i & i < len f holds
b1 . (i + 1) = (b1 /. i) + (f /. (i + 1)) ) )
proof end;
uniqueness
for b1, b2 being FinSequence of REAL n st len f = len b1 & f . 1 = b1 . 1 & ( for i being Nat st 1 <= i & i < len f holds
b1 . (i + 1) = (b1 /. i) + (f /. (i + 1)) ) & len f = len b2 & f . 1 = b2 . 1 & ( for i being Nat st 1 <= i & i < len f holds
b2 . (i + 1) = (b2 /. i) + (f /. (i + 1)) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def10 defines accum EUCLID_7:def 10 :
for n being Nat
for f, b3 being FinSequence of REAL n holds
( b3 = accum f iff ( len f = len b3 & f . 1 = b3 . 1 & ( for i being Nat st 1 <= i & i < len f holds
b3 . (i + 1) = (b3 /. i) + (f /. (i + 1)) ) ) );

definition
let n be Nat;
let f be FinSequence of REAL n;
func Sum f -> Element of REAL n equals :Def11: :: EUCLID_7:def 11
(accum f) . (len f) if len f > 0
otherwise 0* n;
coherence
( ( len f > 0 implies (accum f) . (len f) is Element of REAL n ) & ( not len f > 0 implies 0* n is Element of REAL n ) )
proof end;
consistency
for b1 being Element of REAL n holds verum
;
end;

:: deftheorem Def11 defines Sum EUCLID_7:def 11 :
for n being Nat
for f being FinSequence of REAL n holds
( ( len f > 0 implies Sum f = (accum f) . (len f) ) & ( not len f > 0 implies Sum f = 0* n ) );

theorem Th21: :: EUCLID_7:21
for n being Nat
for F, F2 being FinSequence of REAL n
for h being Permutation of (dom F) st F2 = F (*) h holds
Sum F2 = Sum F
proof end;

theorem Th22: :: EUCLID_7:22
for n being Nat
for k being Element of NAT holds Sum (k |-> (0* n)) = 0* n
proof end;

theorem Th23: :: EUCLID_7:23
for n being Nat
for g being FinSequence of REAL n
for h being FinSequence of NAT
for F being FinSequence of REAL n st h is increasing & rng h c= dom g & F = g * h & ( for i being Element of NAT st i in dom g & not i in rng h holds
g . i = 0* n ) holds
Sum g = Sum F
proof end;

theorem Th24: :: EUCLID_7:24
for n being Nat
for g being FinSequence of REAL n
for h being FinSequence of NAT
for F being FinSequence of REAL n st h is one-to-one & rng h c= dom g & F = g * h & ( for i being Element of NAT st i in dom g & not i in rng h holds
g . i = 0* n ) holds
Sum g = Sum F
proof end;

begin

definition
let n, i be Nat;
:: original: Base_FinSeq
redefine func Base_FinSeq (n,i) -> Element of REAL n;
coherence
Base_FinSeq (n,i) is Element of REAL n
proof end;
end;

theorem Th25: :: EUCLID_7:25
for n, i1, i2 being Nat st 1 <= i1 & i1 <= n & Base_FinSeq (n,i1) = Base_FinSeq (n,i2) holds
i1 = i2
proof end;

theorem Th26: :: EUCLID_7:26
for n, i being Nat holds sqr (Base_FinSeq (n,i)) = Base_FinSeq (n,i)
proof end;

theorem Th27: :: EUCLID_7:27
for i, n being Nat st 1 <= i & i <= n holds
Sum (Base_FinSeq (n,i)) = 1
proof end;

theorem Th28: :: EUCLID_7:28
for i, n being Nat st 1 <= i & i <= n holds
|.(Base_FinSeq (n,i)).| = 1
proof end;

theorem Th29: :: EUCLID_7:29
for i, n, j being Nat st 1 <= i & i <= n & i <> j holds
|((Base_FinSeq (n,i)),(Base_FinSeq (n,j)))| = 0
proof end;

theorem Th30: :: EUCLID_7:30
for n, i being Nat
for x being Element of REAL n st 1 <= i & i <= n holds
|(x,(Base_FinSeq (n,i)))| = x . i
proof end;

definition
let n be Nat;
let x0 be Element of REAL n;
func ProjFinSeq x0 -> FinSequence of REAL n means :Def12: :: EUCLID_7:def 12
( len it = n & ( for i being Nat st 1 <= i & i <= n holds
it . i = |(x0,(Base_FinSeq (n,i)))| * (Base_FinSeq (n,i)) ) );
existence
ex b1 being FinSequence of REAL n st
( len b1 = n & ( for i being Nat st 1 <= i & i <= n holds
b1 . i = |(x0,(Base_FinSeq (n,i)))| * (Base_FinSeq (n,i)) ) )
proof end;
uniqueness
for b1, b2 being FinSequence of REAL n st len b1 = n & ( for i being Nat st 1 <= i & i <= n holds
b1 . i = |(x0,(Base_FinSeq (n,i)))| * (Base_FinSeq (n,i)) ) & len b2 = n & ( for i being Nat st 1 <= i & i <= n holds
b2 . i = |(x0,(Base_FinSeq (n,i)))| * (Base_FinSeq (n,i)) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def12 defines ProjFinSeq EUCLID_7:def 12 :
for n being Nat
for x0 being Element of REAL n
for b3 being FinSequence of REAL n holds
( b3 = ProjFinSeq x0 iff ( len b3 = n & ( for i being Nat st 1 <= i & i <= n holds
b3 . i = |(x0,(Base_FinSeq (n,i)))| * (Base_FinSeq (n,i)) ) ) );

theorem Th31: :: EUCLID_7:31
for n being Nat
for x0 being Element of REAL n holds x0 = Sum (ProjFinSeq x0)
proof end;

definition
let n be Nat;
func RN_Base n -> Subset of (REAL n) equals :: EUCLID_7:def 13
{ (Base_FinSeq (n,i)) where i is Element of NAT : ( 1 <= i & i <= n ) } ;
coherence
{ (Base_FinSeq (n,i)) where i is Element of NAT : ( 1 <= i & i <= n ) } is Subset of (REAL n)
proof end;
end;

:: deftheorem defines RN_Base EUCLID_7:def 13 :
for n being Nat holds RN_Base n = { (Base_FinSeq (n,i)) where i is Element of NAT : ( 1 <= i & i <= n ) } ;

theorem Th32: :: EUCLID_7:32
for n being non zero Nat holds RN_Base n <> {}
proof end;

registration
cluster RN_Base 0 -> empty ;
coherence
RN_Base 0 is empty
proof end;
end;

registration
let n be non zero Nat;
cluster RN_Base n -> non empty ;
coherence
not RN_Base n is empty
by Th32;
end;

registration
let n be Nat;
cluster RN_Base n -> orthogonal_basis ;
coherence
RN_Base n is orthogonal_basis
proof end;
end;

registration
let n be Nat;
cluster functional FinSequence-membered orthogonal_basis for Element of bool (REAL n);
existence
ex b1 being Subset of (REAL n) st b1 is orthogonal_basis
proof end;
end;

definition
let n be Nat;
mode Orthogonal_Basis of n is orthogonal_basis Subset of (REAL n);
end;

registration
let n be non zero Nat;
cluster orthogonal_basis -> non empty for Element of bool (REAL n);
coherence
for b1 being Orthogonal_Basis of n holds not b1 is empty
proof end;
end;

begin

registration
let n be Element of NAT ;
cluster REAL-US n -> constituted-FinSeqs ;
coherence
REAL-US n is constituted-FinSeqs
proof end;
end;

registration
let n be Element of NAT ;
cluster -> real-valued for Element of the carrier of (REAL-US n);
coherence
for b1 being Element of (REAL-US n) holds b1 is real-valued
proof end;
end;

registration
let n be Element of NAT ;
let x, y be VECTOR of (REAL-US n);
let a, b be real-valued Function;
identify x + y with a + b when x = a, y = b;
compatibility
( x = a & y = b implies x + y = a + b )
proof end;
end;

registration
let n be Element of NAT ;
let x be VECTOR of (REAL-US n);
let y be real-valued Function;
let a, b be Element of REAL ;
identify a * x with b * y when x = y, a = b;
compatibility
( x = y & a = b implies a * x = b * y )
proof end;
end;

registration
let n be Element of NAT ;
let x be VECTOR of (REAL-US n);
let a be real-valued Function;
identify - x with - a when x = a;
compatibility
( x = a implies - x = - a )
proof end;
end;

registration
let n be Element of NAT ;
let x, y be VECTOR of (REAL-US n);
let a, b be real-valued Function;
identify x - y with a - b when x = a, y = b;
compatibility
( x = a & y = b implies x - y = a - b )
;
end;

theorem Th33: :: EUCLID_7:33
for n, j being Element of NAT
for F being FinSequence of the carrier of (REAL-US n)
for Bn being Subset of (REAL-US n)
for v0 being Element of (REAL-US n)
for l being Linear_Combination of Bn st F is one-to-one & Bn is R-orthogonal & rng F = Carrier l & v0 in Bn & j in dom (l (#) F) & v0 = F . j holds
(Euclid_scalar n) . (v0,(Sum (l (#) F))) = (Euclid_scalar n) . (v0,((l . (F /. j)) * v0))
proof end;

theorem Th34: :: EUCLID_7:34
for n being Element of NAT
for f being FinSequence of REAL n
for g being FinSequence of the carrier of (REAL-US n) st f = g holds
Sum f = Sum g
proof end;

registration
let A be set ;
cluster RealVectSpace A -> constituted-Functions ;
coherence
RealVectSpace A is constituted-Functions
proof end;
end;

registration
let n be Nat;
cluster RealVectSpace (Seg n) -> constituted-FinSeqs ;
coherence
RealVectSpace (Seg n) is constituted-FinSeqs
proof end;
end;

registration
let A be set ;
cluster -> real-valued for Element of the carrier of (RealVectSpace A);
coherence
for b1 being Element of (RealVectSpace A) holds b1 is real-valued
proof end;
end;

registration
let A be set ;
let x, y be VECTOR of (RealVectSpace A);
let a, b be real-valued Function;
identify x + y with a + b when x = a, y = b;
compatibility
( x = a & y = b implies x + y = a + b )
proof end;
end;

registration
let A be set ;
let x be VECTOR of (RealVectSpace A);
let y be real-valued Function;
let a, b be Element of REAL ;
identify a * x with b * y when x = y, a = b;
compatibility
( x = y & a = b implies a * x = b * y )
proof end;
end;

registration
let A be set ;
let x be VECTOR of (RealVectSpace A);
let a be real-valued Function;
identify - x with - a when x = a;
compatibility
( x = a implies - x = - a )
proof end;
end;

registration
let A be set ;
let x, y be VECTOR of (RealVectSpace A);
let a, b be real-valued Function;
identify x - y with a - b when x = a, y = b;
compatibility
( x = a & y = b implies x - y = a - b )
;
end;

theorem Th35: :: EUCLID_7:35
for n being Nat
for X being Subspace of RealVectSpace (Seg n)
for x being Element of REAL n
for a being Real st x in the carrier of X holds
a * x in the carrier of X
proof end;

theorem Th36: :: EUCLID_7:36
for n being Nat
for X being Subspace of RealVectSpace (Seg n)
for x, y being Element of REAL n st x in the carrier of X & y in the carrier of X holds
x + y in the carrier of X
proof end;

theorem :: EUCLID_7:37
for n being Nat
for X being Subspace of RealVectSpace (Seg n)
for x, y being Element of REAL n
for a, b being Real st x in the carrier of X & y in the carrier of X holds
(a * x) + (b * y) in the carrier of X
proof end;

Lm3: for n being Nat
for X being Subspace of RealVectSpace (Seg n)
for x, y being Element of REAL n
for a being Real st x in the carrier of X & y in the carrier of X holds
(a * x) + y in the carrier of X

proof end;

theorem :: EUCLID_7:38
for n being Nat
for u, v being Element of REAL n holds (Euclid_scalar n) . (u,v) = |(u,v)| by REAL_NS1:def 5;

theorem Th39: :: EUCLID_7:39
for n, j being Nat
for F being FinSequence of the carrier of (RealVectSpace (Seg n))
for Bn being Subset of (RealVectSpace (Seg n))
for v0 being Element of (RealVectSpace (Seg n))
for l being Linear_Combination of Bn st F is one-to-one & Bn is R-orthogonal & rng F = Carrier l & v0 in Bn & j in dom (l (#) F) & v0 = F . j holds
(Euclid_scalar n) . (v0,(Sum (l (#) F))) = (Euclid_scalar n) . (v0,((l . (F /. j)) * v0))
proof end;

registration
let n be Nat;
cluster R-orthonormal -> linearly-independent for Element of bool the carrier of (RealVectSpace (Seg n));
coherence
for b1 being Subset of (RealVectSpace (Seg n)) st b1 is R-orthonormal holds
b1 is linearly-independent
proof end;
end;

registration
let n be Element of NAT ;
cluster R-orthonormal -> linearly-independent for Element of bool the carrier of (REAL-US n);
coherence
for b1 being Subset of (REAL-US n) st b1 is R-orthonormal holds
b1 is linearly-independent
proof end;
end;

theorem Th40: :: EUCLID_7:40
for n being Nat
for Bn being Subset of (RealVectSpace (Seg n))
for x, y being Element of REAL n
for a being Real st Bn is linearly-independent & x in Bn & y in Bn & y = a * x holds
x = y
proof end;

Lm4: now :: thesis: for n being Nat holds
( RN_Base n is finite & card (RN_Base n) = n )
let n be Nat; :: thesis: ( RN_Base n is finite & card (RN_Base n) = n )
thus ( RN_Base n is finite & card (RN_Base n) = n ) :: thesis: verum
proof
per cases ( n is empty or not n is empty ) ;
suppose n is empty ; :: thesis: ( RN_Base n is finite & card (RN_Base n) = n )
hence ( RN_Base n is finite & card (RN_Base n) = n ) ; :: thesis: verum
end;
suppose not n is empty ; :: thesis: ( RN_Base n is finite & card (RN_Base n) = n )
then reconsider n = n as non empty Nat ;
defpred S1[ set , set ] means for i being Element of NAT st i = $1 holds
$2 = Base_FinSeq (n,i);
A1: for x being set st x in Seg n holds
ex y being set st S1[x,y]
proof
let x be set ; :: thesis: ( x in Seg n implies ex y being set st S1[x,y] )
assume x in Seg n ; :: thesis: ex y being set st S1[x,y]
then reconsider j = x as Element of NAT ;
for i being Element of NAT st i = j holds
Base_FinSeq (n,j) = Base_FinSeq (n,i) ;
hence ex y being set st S1[x,y] ; :: thesis: verum
end;
consider f being Function such that
A2: ( dom f = Seg n & ( for x2 being set st x2 in Seg n holds
S1[x2,f . x2] ) ) from CLASSES1:sch 1(A1);
A3: rng f c= RN_Base n
proof
let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng f or y in RN_Base n )
assume y in rng f ; :: thesis: y in RN_Base n
then consider x being set such that
A4: x in dom f and
A5: y = f . x by FUNCT_1:def 3;
reconsider nx = x as Element of NAT by A2, A4;
A6: nx <= n by A2, A4, FINSEQ_1:1;
A7: f . x = Base_FinSeq (n,nx) by A2, A4;
1 <= nx by A2, A4, FINSEQ_1:1;
hence y in RN_Base n by A5, A6, A7; :: thesis: verum
end;
then reconsider f2 = f as Function of (Seg n),(RN_Base n) by A2, FUNCT_2:2;
for x1, x2 being set st x1 in dom f & x2 in dom f & f . x1 = f . x2 holds
x1 = x2
proof
let x1, x2 be set ; :: thesis: ( x1 in dom f & x2 in dom f & f . x1 = f . x2 implies x1 = x2 )
assume that
A8: x1 in dom f and
A9: x2 in dom f and
A10: f . x1 = f . x2 ; :: thesis: x1 = x2
reconsider nx1 = x1, nx2 = x2 as Element of NAT by A2, A8, A9;
A11: nx1 <= n by A2, A8, FINSEQ_1:1;
A12: f . x2 = Base_FinSeq (n,nx2) by A2, A9;
A13: f . x1 = Base_FinSeq (n,nx1) by A2, A8;
1 <= nx1 by A2, A8, FINSEQ_1:1;
hence x1 = x2 by A10, A11, A13, A12, Th25; :: thesis: verum
end;
then A14: f2 is one-to-one by FUNCT_1:def 4;
RN_Base n c= rng f
proof
let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in RN_Base n or y in rng f )
assume y in RN_Base n ; :: thesis: y in rng f
then consider i being Element of NAT such that
A15: y = Base_FinSeq (n,i) and
A16: 1 <= i and
A17: i <= n ;
A18: i in Seg n by A16, A17, FINSEQ_1:1;
then f . i = Base_FinSeq (n,i) by A2;
hence y in rng f by A2, A15, A18, FUNCT_1:def 3; :: thesis: verum
end;
then rng f = RN_Base n by A3, XBOOLE_0:def 10;
then f2 is onto by FUNCT_2:def 3;
then card (Seg n) = card (RN_Base n) by A14, Lm1;
hence ( RN_Base n is finite & card (RN_Base n) = n ) by FINSEQ_1:57; :: thesis: verum
end;
end;
end;
end;

begin

registration
let n be Nat;
cluster RN_Base n -> finite ;
coherence
RN_Base n is finite
by Lm4;
end;

theorem :: EUCLID_7:41
for n being Nat holds card (RN_Base n) = n by Lm4;

theorem Th42: :: EUCLID_7:42
for n being Nat
for f being FinSequence of REAL n
for g being FinSequence of the carrier of (RealVectSpace (Seg n)) st f = g holds
Sum f = Sum g
proof end;

theorem Th43: :: EUCLID_7:43
for n being Nat
for x0 being Element of (RealVectSpace (Seg n))
for B being Subset of (RealVectSpace (Seg n)) st B = RN_Base n holds
ex l being Linear_Combination of B st x0 = Sum l
proof end;

theorem Th44: :: EUCLID_7:44
for n being Element of NAT
for x0 being Element of (REAL-US n)
for B being Subset of (REAL-US n) st B = RN_Base n holds
ex l being Linear_Combination of B st x0 = Sum l
proof end;

theorem Th45: :: EUCLID_7:45
for n being Nat
for B being Subset of (RealVectSpace (Seg n)) st B = RN_Base n holds
B is Basis of RealVectSpace (Seg n)
proof end;

registration
let n be Nat;
cluster RealVectSpace (Seg n) -> finite-dimensional ;
coherence
RealVectSpace (Seg n) is finite-dimensional
proof end;
end;

theorem :: EUCLID_7:46
for n being Nat holds dim (RealVectSpace (Seg n)) = n
proof end;

theorem Th47: :: EUCLID_7:47
for n being Nat
for B being Subset of (RealVectSpace (Seg n)) st B is Basis of RealVectSpace (Seg n) holds
card B = n
proof end;

theorem Th48: :: EUCLID_7:48
{} is Basis of RealVectSpace (Seg 0)
proof end;

theorem Th49: :: EUCLID_7:49
for n being Element of NAT holds RN_Base n is Basis of REAL-US n
proof end;

theorem Th50: :: EUCLID_7:50
for n being Nat
for D being Orthogonal_Basis of n holds D is Basis of RealVectSpace (Seg n)
proof end;

registration
let n be Element of NAT ;
cluster REAL-US n -> finite-dimensional ;
coherence
REAL-US n is finite-dimensional
proof end;
end;

theorem :: EUCLID_7:51
for n being Element of NAT holds dim (REAL-US n) = n
proof end;

theorem :: EUCLID_7:52
for n being Nat
for B being Orthogonal_Basis of n holds card B = n
proof end;