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

theorem :: EUCLID_7:1
canceled;

::$CT theorem Th1: :: 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 Th4: :: 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 m, n 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 :: 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 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 Th5: :: 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 Th6: :: 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 Th7: :: 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 Th8: :: 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 Th9: :: 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 Th10: :: EUCLID_7:11 {} is Permutation of {} proof end; theorem :: EUCLID_7:12 <*1*> is Permutation of {1} proof end; theorem Th12: :: 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 Th13: :: 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; 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 coherence for b1 being set st b1 is empty holds b1 is R-orthogonal ; 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 ; end; registration 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 Th15: :: EUCLID_7:16 for f being real-valued FinSequence st |.f.| = 1 holds {f} is R-normal by TARSKI:def 1; theorem Th16: :: 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 :: EUCLID_7:def 5 ( B0 is R-orthogonal & B0 is R-normal ); end; :: deftheorem 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 coherence for b1 being set st b1 is R-orthonormal holds ( b1 is R-orthogonal & b1 is R-normal ) ; coherence for b1 being set st b1 is R-orthogonal & b1 is R-normal holds b1 is R-orthonormal ; end; registration coherence 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; 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 :: EUCLID_7:def 7 ( B0 is R-orthonormal & B0 is complete ); end; :: deftheorem 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; coherence for b1 being Subset of (REAL n) st b1 is orthogonal_basis holds ( b1 is R-orthonormal & b1 is complete ) ; coherence for b1 being Subset of (REAL n) st b1 is R-orthonormal & b1 is complete holds b1 is orthogonal_basis ; end; theorem Th17: :: EUCLID_7:18 for B0 being Subset of () 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; definition let n be Nat; let X be Subset of (REAL n); attr X is linear_manifold means :: 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 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; coherence [#] (REAL n) is linear_manifold proof end; end; theorem Th19: :: 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 Th19; 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); coherence 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 () . (len f) if len f > 0 otherwise 0* n; coherence ( ( len f > 0 implies () . (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 = () . (len f) ) & ( not len f > 0 implies Sum f = 0* n ) ); theorem Th20: :: 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 Th21: :: EUCLID_7:22 for n being Nat for k being Element of NAT holds Sum (k |-> (0* n)) = 0* n proof end; theorem Th22: :: 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 Th23: :: 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; 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 Th24: :: 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 Th25: :: EUCLID_7:26 for i, n being Nat holds sqr (Base_FinSeq (n,i)) = Base_FinSeq (n,i) proof end; Lm3: by XREAL_0:def 1; theorem Th26: :: EUCLID_7:27 for i, n being Nat st 1 <= i & i <= n holds Sum (Base_FinSeq (n,i)) = 1 proof end; theorem Th27: :: EUCLID_7:28 for i, n being Nat st 1 <= i & i <= n holds |.(Base_FinSeq (n,i)).| = 1 proof end; theorem Th28: :: EUCLID_7:29 for i, j, n being Nat st 1 <= i & i <= n & i <> j holds |((Base_FinSeq (n,i)),(Base_FinSeq (n,j)))| = 0 proof end; theorem Th29: :: EUCLID_7:30 for i, n 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 Th30: :: EUCLID_7:31 for n being Nat for x0 being Element of REAL n holds x0 = Sum () 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 Th31: :: EUCLID_7:32 for n being non zero Nat holds RN_Base n <> {} proof end; registration coherence proof end; end; registration let n be non zero Nat; cluster RN_Base n -> non empty ; coherence not RN_Base n is empty by Th31; end; registration let n be Nat; coherence proof end; end; registration let n be Nat; existence ex b1 being Subset of (REAL n) st b1 is orthogonal_basis proof end; end; definition 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; registration let n be Element of NAT ; coherence proof end; end; registration let n be Element of NAT ; cluster -> real-valued for Element of the carrier of (); coherence for b1 being Element of () holds b1 is real-valued proof end; end; registration let n be Element of NAT ; let x, y be VECTOR of (); 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 (); 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 (); 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 (); 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 Th32: :: EUCLID_7:33 for n, j being Element of NAT for F being FinSequence of the carrier of () for Bn being Subset of () for v0 being Element of () 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 () . (v0,(Sum (l (#) F))) = () . (v0,((l . (F /. j)) * v0)) proof end; theorem Th33: :: EUCLID_7:34 for n being Element of NAT for f being FinSequence of REAL n for g being FinSequence of the carrier of () st f = g holds Sum f = Sum g proof end; registration let A be set ; coherence ; end; registration let n be Nat; coherence proof end; end; registration let A be set ; cluster -> real-valued for Element of the carrier of (); coherence for b1 being Element of () holds b1 is real-valued proof end; end; registration let A be set ; let x, y be VECTOR of (); 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 (); 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 (); 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 (); 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 Th34: :: 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 Th35: :: 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; Lm4: 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 () . (u,v) = |(u,v)| by REAL_NS1:def 5; theorem Th38: :: EUCLID_7:39 for j, n 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 () . (v0,(Sum (l (#) F))) = () . (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 (); coherence for b1 being Subset of () st b1 is R-orthonormal holds b1 is linearly-independent proof end; end; theorem Th39: :: 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; Lm5: now :: thesis: for n being Nat holds ( RN_Base n is finite & card () = n ) let n be Nat; :: thesis: ( RN_Base n is finite & card () = n ) thus ( RN_Base n is finite & card () = n ) :: thesis: verum proof per cases ( n is zero or not n is zero ) ; suppose n is zero ; :: thesis: ( RN_Base n is finite & card () = n ) hence ( RN_Base n is finite & card () = n ) ; :: thesis: verum end; suppose not n is zero ; :: thesis: ( RN_Base n is finite & card () = n ) then reconsider n = n as non zero Nat ; defpred S1[ object , object ] means for i being Element of NAT st i =$1 holds
\$2 = Base_FinSeq (n,i);
A1: for x being object st x in Seg n holds
ex y being object st S1[x,y]
proof
let x be object ; :: thesis: ( x in Seg n implies ex y being object st S1[x,y] )
assume x in Seg n ; :: thesis: ex y being object 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 object st S1[x,y] ; :: thesis: verum
end;
consider f being Function such that
A2: ( dom f = Seg n & ( for x2 being object st x2 in Seg n holds
S1[x2,f . x2] ) ) from A3: rng f c= RN_Base n
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng f or y in RN_Base n )
assume y in rng f ; :: thesis:
then consider x being object 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 ;
A7: f . x = Base_FinSeq (n,nx) by A2, A4;
1 <= nx by ;
hence y in RN_Base n by A5, A6, A7; :: thesis: verum
end;
then reconsider f2 = f as Function of (Seg n),() by ;
for x1, x2 being object st x1 in dom f & x2 in dom f & f . x1 = f . x2 holds
x1 = x2
proof
let x1, x2 be object ; :: 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 ;
A12: f . x2 = Base_FinSeq (n,nx2) by A2, A9;
A13: f . x1 = Base_FinSeq (n,nx1) by A2, A8;
1 <= nx1 by ;
hence x1 = x2 by A10, A11, A13, A12, Th24; :: 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 object ; :: 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 ;
then f . i = Base_FinSeq (n,i) by A2;
hence y in rng f by ; :: thesis: verum
end;
then rng f = RN_Base n by ;
then f2 is onto by FUNCT_2:def 3;
then card (Seg n) = card () by ;
hence ( RN_Base n is finite & card () = n ) by FINSEQ_1:57; :: thesis: verum
end;
end;
end;
end;

registration
let n be Nat;
coherence by Lm5;
end;

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

theorem Th41: :: 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 Th42: :: 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 Th43: :: EUCLID_7:44
for n being Element of NAT
for x0 being Element of ()
for B being Subset of () st B = RN_Base n holds
ex l being Linear_Combination of B st x0 = Sum l
proof end;

theorem Th44: :: 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;
coherence
proof end;
end;

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

theorem Th46: :: 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 Th47: :: EUCLID_7:48
{} is Basis of RealVectSpace ()
proof end;

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

theorem Th49: :: 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 ;
coherence
proof end;
end;

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

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