:: 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))
proofend;

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

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*>
proofend;

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

registration
let f1, f2 be FinSequence;
cluster<:f1,f2:> ->  FinSequence-like ;
coherence
 <:f1,f2:> is FinSequence-like
proofend;
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:]
proofend;
end;

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

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 &amp; i < len h holds
h . i < h . (i + 1);
compatibility
 ( h is increasing iff for i being Nat st 1 <= i &amp; i < len h holds
h . i < h . (i + 1) )
proofend;
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 &amp; 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 &amp; 1 <= i &amp; j <= len h holds
h . i < h . j
proofend;

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

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

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

definition
let D be set ;
let F be FinSequence of D;
let h be Permutation of (dom F);
funcF (*) h ->  FinSequence of D equals :: EUCLID_7:def 2
F * h;
coherence
 F * h is FinSequence of D
proofend;
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 &amp; i <= len f &amp; 1 <= j &amp; j <= len f holds
( (Swap (f,i,j)) . i = f . j &amp; (Swap (f,i,j)) . j = f . i )
proofend;

theorem Th11: :: EUCLID_7:11
{} is Permutation of {}
proofend;

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

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 )
proofend;

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 &amp; h2 is increasing &amp; dom h = dom h2 &amp; rng h = rng h2 )
proofend;

begin

definition
let B0 be set ;
attrB0 is R-orthogonal  means :Def3: :: EUCLID_7:def 3
 for x, y being real-valued FinSequence st x in B0 &amp; y in B0 &amp; 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 &amp; y in B0 &amp; 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
proofend;
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 &amp; y in B0 &amp; x <> y holds
x,y are_orthogonal )
proofend;

definition
let B0 be set ;
attrB0 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
proofend;
end;

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

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

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

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

definition
let B0 be set ;
attrB0 is R-orthonormal  means :Def5: :: EUCLID_7:def 5
( B0 is R-orthogonal &amp; 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 &amp; 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 &amp; 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 &amp; b1 is R-normal holds
b1 is R-orthonormal by Def5;
end;

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

registration
cluster non empty R-orthonormal for set ;
existence
 ex b1 being set st
( b1 is R-orthonormal &amp; not b1 is empty )
proofend;
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
proofend;
end;

definition
let n be Nat;
let B0 be Subset of (REAL n);
attrB0 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);
attrB0 is orthogonal_basis  means :Def7: :: EUCLID_7:def 7
( B0 is R-orthonormal &amp; 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 &amp; 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 &amp; 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 &amp; 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 = {}
proofend;

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 &amp; ( for x being Element of REAL n st x in B0 holds
|(x,y)| = 0 ) holds
y = 0* n
proofend;

begin

definition
let n be Nat;
let X be Subset of (REAL n);
attrX 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 &amp; 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 &amp; 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
proofend;
end;

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

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 &amp; X c= Y )  }  ;
correctness
coherence
meet  {  Y where Y is Subset of (REAL n) : ( Y is linear_manifold &amp; X c= Y )  }  is Subset of (REAL n);
proofend;
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 &amp; 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
proofend;
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 &amp; f . 1 = it . 1 &amp; ( for i being Nat st 1 <= i &amp; 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 &amp; f . 1 = b1 . 1 &amp; ( for i being Nat st 1 <= i &amp; i < len f holds
b1 . (i + 1) = (b1 /. i) + (f /. (i + 1)) ) )
proofend;
uniqueness
 for b1, b2 being FinSequence of REAL n st len f = len b1 &amp; f . 1 = b1 . 1 &amp; ( for i being Nat st 1 <= i &amp; i < len f holds
b1 . (i + 1) = (b1 /. i) + (f /. (i + 1)) ) &amp; len f = len b2 &amp; f . 1 = b2 . 1 &amp; ( for i being Nat st 1 <= i &amp; i < len f holds
b2 . (i + 1) = (b2 /. i) + (f /. (i + 1)) ) holds
b1 = b2
proofend;
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 &amp; f . 1 = b3 . 1 &amp; ( for i being Nat st 1 <= i &amp; 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 ) &amp; ( not len f > 0 implies 0* n is Element of REAL n ) )
proofend;
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) ) &amp; ( 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
proofend;

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

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 &amp; rng h c= dom g &amp; F = g * h &amp; ( for i being Element of NAT st i in dom g &amp; not i in rng h holds
g . i = 0* n ) holds
Sum g = Sum F
proofend;

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 &amp; rng h c= dom g &amp; F = g * h &amp; ( for i being Element of NAT st i in dom g &amp; not i in rng h holds
g . i = 0* n ) holds
Sum g = Sum F
proofend;

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
proofend;
end;

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

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

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

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

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

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

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 &amp; ( for i being Nat st 1 <= i &amp; 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 &amp; ( for i being Nat st 1 <= i &amp; i <= n holds
b1 . i = |(x0,(Base_FinSeq (n,i)))| * (Base_FinSeq (n,i)) ) )
proofend;
uniqueness
 for b1, b2 being FinSequence of REAL n st len b1 = n &amp; ( for i being Nat st 1 <= i &amp; i <= n holds
b1 . i = |(x0,(Base_FinSeq (n,i)))| * (Base_FinSeq (n,i)) ) &amp; len b2 = n &amp; ( for i being Nat st 1 <= i &amp; i <= n holds
b2 . i = |(x0,(Base_FinSeq (n,i)))| * (Base_FinSeq (n,i)) ) holds
b1 = b2
proofend;
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 &amp; ( for i being Nat st 1 <= i &amp; 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)
proofend;

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 &amp; i <= n )  }  ;
coherence
  {  (Base_FinSeq (n,i)) where i is Element of NAT : ( 1 <= i &amp; i <= n )  }  is Subset of (REAL n)
proofend;
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 &amp; i <= n )  }  ;

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

registration
cluster RN_Base 0 ->  empty ;
coherence
 RN_Base 0 is empty
proofend;
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
proofend;
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
proofend;
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
proofend;
end;

begin

registration
let n be Element of NAT ;
cluster REAL-US n ->  constituted-FinSeqs ;
coherence
 REAL-US n is constituted-FinSeqs
proofend;
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
proofend;
end;

registration
let n be Element of NAT ;
let x, y be VECTOR of (REAL-US n);
let a, b be real-valued Function;
identifyx + y with a + b when x = a, y = b;
compatibility
 ( x = a &amp; y = b implies x + y = a + b )
proofend;
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 ;
identifya * x with b * y when x = y, a = b;
compatibility
 ( x = y &amp; a = b implies a * x = b * y )
proofend;
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 )
proofend;
end;

registration
let n be Element of NAT ;
let x, y be VECTOR of (REAL-US n);
let a, b be real-valued Function;
identifyx - y with a - b when x = a, y = b;
compatibility
 ( x = a &amp; 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 &amp; Bn is R-orthogonal &amp; rng F = Carrier l &amp; v0 in Bn &amp; j in dom (l (#) F) &amp; v0 = F . j holds
(Euclid_scalar n) . (v0,(Sum (l (#) F))) = (Euclid_scalar n) . (v0,((l . (F /. j)) * v0))
proofend;

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

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

registration
let n be Nat;
cluster RealVectSpace (Seg n) ->  constituted-FinSeqs ;
coherence
 RealVectSpace (Seg n) is constituted-FinSeqs
proofend;
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
proofend;
end;

registration
let A be set ;
let x, y be VECTOR of (RealVectSpace A);
let a, b be real-valued Function;
identifyx + y with a + b when x = a, y = b;
compatibility
 ( x = a &amp; y = b implies x + y = a + b )
proofend;
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 ;
identifya * x with b * y when x = y, a = b;
compatibility
 ( x = y &amp; a = b implies a * x = b * y )
proofend;
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 )
proofend;
end;

registration
let A be set ;
let x, y be VECTOR of (RealVectSpace A);
let a, b be real-valued Function;
identifyx - y with a - b when x = a, y = b;
compatibility
 ( x = a &amp; 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
proofend;

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 &amp; y in the carrier of X holds
x + y in the carrier of X
proofend;

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 &amp; y in the carrier of X holds
(a * x) + (b * y) in the carrier of X
proofend;

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 &amp; y in the carrier of X holds
(a * x) + y in the carrier of X
proofend;

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 &amp; Bn is R-orthogonal &amp; rng F = Carrier l &amp; v0 in Bn &amp; j in dom (l (#) F) &amp; v0 = F . j holds
(Euclid_scalar n) . (v0,(Sum (l (#) F))) = (Euclid_scalar n) . (v0,((l . (F /. j)) * v0))
proofend;

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
proofend;
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
proofend;
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 &amp; x in Bn &amp; y in Bn &amp; y = a * x holds
x = y
proofend;

Lm4: now__::_thesis:_for_n_being_Nat_holds_
(_RN_Base_n_is_finite_&amp;_card_(RN_Base_n)_=_n_)
let n be Nat; ::_thesis: ( RN_Base n is finite &amp; card (RN_Base n) = n )
thus  ( RN_Base n is finite &amp; card (RN_Base n) = n ) ::_thesis: verum
proof
percases ( n is empty or not n is empty ) ;
suppose n is empty ; ::_thesis: ( RN_Base n is finite &amp; card (RN_Base n) = n )
hence  ( RN_Base n is finite &amp; card (RN_Base n) = n ) ; ::_thesis: verum
end;
suppose not n is empty ; ::_thesis: ( RN_Base n is finite &amp; 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 &amp; ( 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 toTARSKI: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 &amp; x2 in dom f &amp; f . x1 = f . x2 holds
x1 = x2
proof
let x1, x2 be set ; ::_thesis: ( x1 in dom f &amp; x2 in dom f &amp; 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 toTARSKI: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 &amp; 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
proofend;

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

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

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)
proofend;

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

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

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

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

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

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

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

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

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