let n be Nat; :: thesis: for D being Orthogonal_Basis of n holds D is Basis of RealVectSpace (Seg n)
let D be Orthogonal_Basis of n; :: thesis: D is Basis of RealVectSpace (Seg n)
set V = RealVectSpace (Seg n);
c1: REAL n = the carrier of (RealVectSpace (Seg n)) by FINSEQ_2:111;
reconsider B = D as R-orthonormal Subset of (RealVectSpace (Seg n)) by FINSEQ_2:111;

per cases ( n = 0 or n <> 0 ) ;

suppose n = 0 ; :: thesis: D is Basis of RealVectSpace (Seg n)

hence D is Basis of RealVectSpace (Seg n) by Th21, Th57; :: thesis: verum

end;

suppose A1: n <> 0 ; :: thesis: D is Basis of RealVectSpace (Seg n)

reconsider D0 = D as R-orthonormal Subset of (REAL n) ;
A3: for D2 being R-orthonormal Subset of (REAL n) st D0 c= D2 holds
D2 = D0 by Def7;
consider I being Basis of RealVectSpace (Seg n) such that
A4: B c= I by RLVECT_5:2;
Lin B is Subspace of Lin I by A4, RLVECT_3:23;
then A5: the carrier of (Lin B) c= the carrier of (Lin I) by RLSUB_1:def 2;
A6: Lin I = RealVectSpace (Seg n) by RLVECT_3:def 3;
card I = n by Th56;
then A7: I is finite ;

A8: now

assume I c= the carrier of (Lin B) ; :: thesis: B is Basis of RealVectSpace (Seg n)
then Lin I is Subspace of Lin B by RLVECT_5:20;
then the carrier of (Lin I) c= the carrier of (Lin B) by RLSUB_1:def 2;
then the carrier of (Lin I) = the carrier of (Lin B) by A5, XBOOLE_0:def 10;
then Lin B = Lin I by RLSUB_1:38;
hence B is Basis of RealVectSpace (Seg n) by A6, RLVECT_3:def 3; :: thesis: verum

end;

now

assume ( B <> I & not I c= the carrier of (Lin B) ) ; :: thesis: B is Basis of RealVectSpace (Seg n)
then consider x0 being set such that
A9: ( x0 in I & not x0 in the carrier of (Lin B) ) by TARSKI:def 3;
not x0 in Lin B by A9, STRUCT_0:def 5;
then A10: ( x0 in I & not x0 in B ) by A9, RLVECT_3:18;
reconsider z0 = x0 as Element of REAL n by A9, FINSEQ_2:111;
A11: I is linearly-independent by RLVECT_3:def 3;
reconsider B1 = B \/ {z0} as Subset of (RealVectSpace (Seg n)) by c1, XBOOLE_1:8;
consider p being FinSequence such that
A12: ( rng p = B & p is one-to-one ) by A4, A7, FINSEQ_4:73;
1 in dom p by A1, A12, FINSEQ_3:34;
then A13: 1 <= len p by FINSEQ_3:27;
reconsider p0 = p as FinSequence of REAL n by A12, FINSEQ_1:def 4;
reconsider a00 = p0 /. 1 as Element of REAL n ;
reconsider z00 = z0 - (|(z0,a00)| * a00) as Element of REAL n ;
set z01 = (1 / |.z00.|) * z00;
defpred S₁[ Nat] means ( 1 <= $1 & $1 <= (len p) + 1 implies ex q being FinSequence of REAL n st
( len q = $1 & ( $1 <= len p implies for d being Real holds not q . $1 = d * (p0 /. $1) ) & q . 1 = z0 & ( for i being Nat
for a, b being Element of REAL n st 1 <= i & i < $1 & a = q /. i & b = p0 /. i holds
( q /. (i + 1) <> 0* n & q . (i + 1) = (q /. i) - (|(a,b)| * (p0 /. i)) ) ) ) );
A14: S₁[ 0 ] ;
A15: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A16: S₁[k] ; :: thesis: S₁[k + 1]

per cases ( ( 1 <= k + 1 & k + 1 <= (len p) + 1 ) or not 1 <= k + 1 or not k + 1 <= (len p) + 1 ) ;

suppose A17: ( 1 <= k + 1 & k + 1 <= (len p) + 1 ) ; :: thesis: S₁[k + 1]

then A18: k <= len p by XREAL_1:8;
k < k + 1 by XREAL_1:31;
then A19: k < (len p) + 1 by A17, XXREAL_0:2;

per cases ( 1 <= k or 1 > k ) ;

suppose 1 <= k ; :: thesis: S₁[k + 1]

then consider q0 being FinSequence of REAL n such that
A20: ( len q0 = k & 1 <= k & k <= (len p) + 1 & ( k <= len p implies for d being Real holds not q0 . k = d * (p0 /. k) ) & q0 . 1 = z0 & ( for i being Nat
for a, b being Element of REAL n st 1 <= i & i < k & a = q0 /. i & b = p0 /. i holds
( q0 /. (i + 1) <> 0* n & q0 . (i + 1) = (q0 /. i) - (|(a,b)| * (p0 /. i)) ) ) ) by A16, A19;
reconsider a2 = q0 /. k, b2 = p0 /. k as Element of REAL n ;
reconsider q3 = <*((q0 /. k) - (|(a2,b2)| * (p0 /. k)))*> as FinSequence of REAL n ;
reconsider q1 = q0 ^ q3 as FinSequence of REAL n ;
A21: len q1 = (len q0) + (len q3) by FINSEQ_1:35
.= k + 1 by A20, FINSEQ_1:57 ;
1 in Seg (len q0) by A20, FINSEQ_1:3;
then A22: 1 in dom q0 by FINSEQ_1:def 3;
then A23: q1 . 1 = z0 by A20, FINSEQ_1:def 7;
A24: 1 <= k + 1 by NAT_1:12;
defpred S₂[ Nat] means ( $1 + 1 <= k + 1 implies not q1 . ($1 + 1) in the carrier of (Lin B) );
A25: S₂[ 0 ] by A9, A20, A22, FINSEQ_1:def 7;
A26: for j being Nat st S₂[j] holds
S₂[j + 1]

proof

let j be Nat; :: thesis: ( S₂[j] implies S₂[j + 1] )
assume A27: S₂[j] ; :: thesis: S₂[j + 1]
( (j + 1) + 1 <= k + 1 implies not q1 . ((j + 1) + 1) in the carrier of (Lin B) )

proof

assume (j + 1) + 1 <= k + 1 ; :: thesis: not q1 . ((j + 1) + 1) in the carrier of (Lin B)
then A28: j + 1 <= k by XREAL_1:8;
A29: B c= the carrier of (Lin B)

proof

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in B or z in the carrier of (Lin B) )
assume z in B ; :: thesis: z in the carrier of (Lin B)
then z in Lin B by RLVECT_3:18;
hence z in the carrier of (Lin B) by STRUCT_0:def 5; :: thesis: verum

end;

per cases ( j + 1 = k or j + 1 < k ) by A28, XXREAL_0:1;

suppose A30: j + 1 = k ; :: thesis: not q1 . ((j + 1) + 1) in the carrier of (Lin B)

then A31: q1 . ((j + 1) + 1) = (q0 /. k) - (|(a2,b2)| * (p0 /. k)) by A20, FINSEQ_1:59;
A32: ( 1 <= j + 1 & j + 1 <= k ) by A30, NAT_1:12;
1 <= (j + 1) + 1 by NAT_1:12;
then A33: q1 /. ((j + 1) + 1) = q1 . ((j + 1) + 1) by A21, A30, FINSEQ_4:24;
j + 1 in dom p0 by A18, A30, A32, FINSEQ_3:27;
then A34: p0 . (j + 1) in rng p by FUNCT_1:def 5;
A35: p0 /. (j + 1) = p0 . (j + 1) by A18, A30, FINSEQ_4:24, NAT_1:12;

now

assume A36: q1 . ((j + 1) + 1) in the carrier of (Lin B) ; :: thesis: contradiction
(q1 /. ((j + 1) + 1)) + (|(a2,b2)| * (p0 /. (j + 1))) = q0 /. (j + 1) by A33, A30, A31, RVSUM_1:64;
then q0 /. (j + 1) in the carrier of (Lin B) by A12, A29, A33, A34, A35, A36, Lm2;
then A37: q0 /. (j + 1) in Lin B by STRUCT_0:def 5;
A38: not q1 . (j + 1) in Lin B by A27, A30, STRUCT_0:def 5, XREAL_1:31;
q1 . (j + 1) = q0 . (j + 1) by A20, A30, FINSEQ_1:85;
hence contradiction by A20, A30, A37, A38, FINSEQ_4:24; :: thesis: verum

end;

hence not q1 . ((j + 1) + 1) in the carrier of (Lin B) ; :: thesis: verum

end;

suppose A39: j + 1 < k ; :: thesis: not q1 . ((j + 1) + 1) in the carrier of (Lin B)

then A40: ( 1 <= j + 1 & j + 1 < k ) by NAT_1:12;
reconsider a11 = q0 /. (j + 1), b11 = p0 /. (j + 1) as Element of REAL n ;
( a11 = q0 /. (j + 1) & b11 = p0 /. (j + 1) ) ;
then A41: ( q0 /. ((j + 1) + 1) <> 0* n & q0 . ((j + 1) + 1) = (q0 /. (j + 1)) - (|(a11,b11)| * (p0 /. (j + 1))) ) by A20, A40;
A42: 1 <= (j + 1) + 1 by NAT_1:12;
A43: (j + 1) + 1 <= k by A39, NAT_1:13;
then A44: q0 /. ((j + 1) + 1) = q0 . ((j + 1) + 1) by A20, A42, FINSEQ_4:24;
A45: j + 1 <= len p0 by A18, A39, XXREAL_0:2;
then j + 1 in dom p0 by A40, FINSEQ_3:27;
then A46: p0 . (j + 1) in rng p by FUNCT_1:def 5;
A47: p0 /. (j + 1) = p0 . (j + 1) by A45, FINSEQ_4:24, NAT_1:12;
A48: q1 . ((j + 1) + 1) = q0 . ((j + 1) + 1) by A20, A42, A43, FINSEQ_1:85;

now

assume A49: q1 . ((j + 1) + 1) in the carrier of (Lin B) ; :: thesis: contradiction
(q0 /. ((j + 1) + 1)) + (|(a11,b11)| * (p0 /. (j + 1))) = q0 /. (j + 1) by A41, A44, RVSUM_1:64;
then q0 /. (j + 1) in the carrier of (Lin B) by A12, A29, A44, A46, A47, A48, A49, Lm2;
then A50: q0 /. (j + 1) in Lin B by STRUCT_0:def 5;
k < k + 1 by XREAL_1:31;
then A51: not q1 . (j + 1) in Lin B by A27, A39, STRUCT_0:def 5, XXREAL_0:2;
A52: 1 <= j + 1 by NAT_1:12;
then q1 . (j + 1) = q0 . (j + 1) by A20, A39, FINSEQ_1:85;
hence contradiction by A20, A39, A50, A51, A52, FINSEQ_4:24; :: thesis: verum

end;

hence not q1 . ((j + 1) + 1) in the carrier of (Lin B) ; :: thesis: verum

end;

end;

end;

hence S₂[j + 1] ; :: thesis: verum

end;

A53: for j being Nat holds S₂[j] from NAT_1:sch 2(A25, A26);
A54: for s1 being Element of (RealVectSpace (Seg n))
for a01 being Real st s1 in B holds
a01 * s1 in the carrier of (Lin B)

proof

let s1 be Element of (RealVectSpace (Seg n)); :: thesis: for a01 being Real st s1 in B holds
a01 * s1 in the carrier of (Lin B)
let a01 be Real; :: thesis: ( s1 in B implies a01 * s1 in the carrier of (Lin B) )
assume A55: s1 in B ; :: thesis: a01 * s1 in the carrier of (Lin B)
{s1} c= B

proof

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in {s1} or z in B )
assume z in {s1} ; :: thesis: z in B
hence z in B by A55, TARSKI:def 1; :: thesis: verum

end;

then Lin {s1} is Subspace of Lin B by RLVECT_3:23;
then A56: the carrier of (Lin {s1}) c= the carrier of (Lin B) by RLSUB_1:def 2;
a01 * s1 in Lin {s1} by RLVECT_4:11;
then a01 * s1 in the carrier of (Lin {s1}) by STRUCT_0:def 5;
hence a01 * s1 in the carrier of (Lin B) by A56; :: thesis: verum

end;

A57: for s1 being Element of REAL n
for a01 being Real st s1 in B holds
a01 * s1 in the carrier of (Lin B)

proof

let s1 be Element of REAL n; :: thesis: for a01 being Real st s1 in B holds
a01 * s1 in the carrier of (Lin B)
let a01 be Real; :: thesis: ( s1 in B implies a01 * s1 in the carrier of (Lin B) )
assume A58: s1 in B ; :: thesis: a01 * s1 in the carrier of (Lin B)
reconsider s10 = s1 as Element of (RealVectSpace (Seg n)) by FINSEQ_2:111;
a01 * s1 = a01 * s10 ;
hence a01 * s1 in the carrier of (Lin B) by A54, A58; :: thesis: verum

end;

A59: ( k + 1 <= len p implies p0 /. (k + 1) in B )

proof

assume A60: k + 1 <= len p ; :: thesis: p0 /. (k + 1) in B
then k + 1 in dom p by A24, FINSEQ_3:27;
then p . (k + 1) in rng p by FUNCT_1:def 5;
hence p0 /. (k + 1) in B by A12, A60, FINSEQ_4:24, NAT_1:12; :: thesis: verum

end;

A61: ( k + 1 <= len p implies for d being Real holds not q1 . (k + 1) = d * (p0 /. (k + 1)) ) by A53, A57, A59;
for i being Nat
for a, b being Element of REAL n st 1 <= i & i < k + 1 & a = q1 /. i & b = p0 /. i holds
( q1 /. (i + 1) <> 0* n & q1 . (i + 1) = (q1 /. i) - (|(a,b)| * (p0 /. i)) )

proof

let i be Nat; :: thesis: for a, b being Element of REAL n st 1 <= i & i < k + 1 & a = q1 /. i & b = p0 /. i holds
( q1 /. (i + 1) <> 0* n & q1 . (i + 1) = (q1 /. i) - (|(a,b)| * (p0 /. i)) )
let a, b be Element of REAL n; :: thesis: ( 1 <= i & i < k + 1 & a = q1 /. i & b = p0 /. i implies ( q1 /. (i + 1) <> 0* n & q1 . (i + 1) = (q1 /. i) - (|(a,b)| * (p0 /. i)) ) )
assume A62: ( 1 <= i & i < k + 1 & a = q1 /. i & b = p0 /. i ) ; :: thesis: ( q1 /. (i + 1) <> 0* n & q1 . (i + 1) = (q1 /. i) - (|(a,b)| * (p0 /. i)) )
then A63: i <= k by NAT_1:13;
A64: 1 <= i + 1 by NAT_1:12;
A65: i + 1 <= k + 1 by A62, NAT_1:13;

per cases ( i < k or i = k ) by A63, XXREAL_0:1;

suppose A66: i < k ; :: thesis: ( q1 /. (i + 1) <> 0* n & q1 . (i + 1) = (q1 /. i) - (|(a,b)| * (p0 /. i)) )

then A67: i + 1 <= k by NAT_1:13;
A68: q1 /. i = q1 . i by A62, A21, FINSEQ_4:24
.= q0 . i by A20, A62, A63, FINSEQ_1:85
.= q0 /. i by A62, A63, A20, FINSEQ_4:24 ;
A69: q1 . (i + 1) = q0 . (i + 1) by A67, A64, A20, FINSEQ_1:85;
A70: q1 /. (i + 1) = q1 . (i + 1) by A64, A65, A21, FINSEQ_4:24;
q0 /. (i + 1) = q0 . (i + 1) by A67, A64, A20, FINSEQ_4:24;
hence ( q1 /. (i + 1) <> 0* n & q1 . (i + 1) = (q1 /. i) - (|(a,b)| * (p0 /. i)) ) by A66, A62, A20, A68, A69, A70; :: thesis: verum

end;

suppose A71: i = k ; :: thesis: ( q1 /. (i + 1) <> 0* n & q1 . (i + 1) = (q1 /. i) - (|(a,b)| * (p0 /. i)) )

A72: k < k + 1 by XREAL_1:31;
A73: len q0 < k + 1 by A20, XREAL_1:31;
A74: q1 . k = q0 . k by A20, FINSEQ_1:85;
A75: q0 /. k = q0 . k by A20, FINSEQ_4:24;
A76: q1 /. k = q1 . k by A20, A21, A72, FINSEQ_4:24;
A77: q1 /. (i + 1) = q1 . (k + 1) by A21, A24, A71, FINSEQ_4:24
.= q3 . ((k + 1) - (len q0)) by A21, A73, FINSEQ_1:37
.= (q0 /. k) - (|(a2,b2)| * (p0 /. k)) by A20, FINSEQ_1:57 ;

now

assume q1 /. (i + 1) = 0* n ; :: thesis: contradiction
then ((q0 /. k) - (|(a2,b2)| * (p0 /. k))) + (|(a2,b2)| * (p0 /. k)) = |(a2,b2)| * (p0 /. k) by A77, EUCLID_4:1;
then A78: q0 /. k = |(a2,b2)| * (p0 /. k) by RVSUM_1:64;
q0 /. k = q0 . k by A20, FINSEQ_4:24;
hence contradiction by A17, A20, A78, XREAL_1:8; :: thesis: verum

end;

hence ( q1 /. (i + 1) <> 0* n & q1 . (i + 1) = (q1 /. i) - (|(a,b)| * (p0 /. i)) ) by A21, A62, A64, A71, A74, A75, A76, A77, FINSEQ_4:24; :: thesis: verum

end;

end;

end;

hence S₁[k + 1] by A21, A23, A61; :: thesis: verum

end;

suppose 1 > k ; :: thesis: S₁[k + 1]

then A79: k = 0 by NAT_1:14;
reconsider q1 = <*z0*> as FinSequence of REAL n ;
A80: ( len q1 = 1 & q1 . 1 = z0 ) by FINSEQ_1:57;
A81: ( 1 <= len p implies for d being Real holds not q1 . 1 = d * (p0 /. 1) )

proof

assume A82: 1 <= len p ; :: thesis: for d being Real holds not q1 . 1 = d * (p0 /. 1)
thus for d being Real holds not q1 . 1 = d * (p0 /. 1) :: thesis: verum

proof

let d be Real; :: thesis: not q1 . 1 = d * (p0 /. 1)
A83: q1 . 1 = z0 by FINSEQ_1:57;
A84: p0 /. 1 = p0 . 1 by A82, FINSEQ_4:24;
1 in dom p0 by A82, FINSEQ_3:27;
then p0 . 1 in B by A12, FUNCT_1:def 5;
hence not q1 . 1 = d * (p0 /. 1) by A4, A10, A11, A83, A84, Th49; :: thesis: verum

end;

end;

for i being Nat
for a, b being Element of REAL n st 1 <= i & i < 1 & a = q1 /. i & b = p0 /. i holds
( q1 /. (i + 1) <> 0* n & q1 . (i + 1) = (q1 /. i) - (|(a,b)| * (p0 /. i)) ) ;
hence S₁[k + 1] by A79, A80, A81; :: thesis: verum

end;

end;

end;

suppose ( not 1 <= k + 1 or not k + 1 <= (len p) + 1 ) ; :: thesis: S₁[k + 1]

hence S₁[k + 1] ; :: thesis: verum

end;

end;

end;

A85: for k being Nat holds S₁[k] from NAT_1:sch 2(A14, A15);
1 <= (len p) + 1 by NAT_1:12;
then consider q being FinSequence of REAL n such that
A86: ( len q = (len p) + 1 & ( (len p) + 1 <= len p implies for d being Real holds not q . ((len p) + 1) = d * (p0 /. ((len p) + 1)) ) & q . 1 = z0 & ( for i being Nat
for a, b being Element of REAL n st 1 <= i & i < (len p) + 1 & a = q /. i & b = p0 /. i holds
( q /. (i + 1) <> 0* n & q . (i + 1) = (q /. i) - (|(a,b)| * (p0 /. i)) ) ) ) by A85;
reconsider u4 = q /. (len q) as Element of REAL n ;
A87: for i being Nat
for s being Element of REAL n st 1 <= i & i <= len p & p0 /. i = s holds
|(s,u4)| = 0

proof

let i be Nat; :: thesis: for s being Element of REAL n st 1 <= i & i <= len p & p0 /. i = s holds
|(s,u4)| = 0
let s be Element of REAL n; :: thesis: ( 1 <= i & i <= len p & p0 /. i = s implies |(s,u4)| = 0 )
assume A88: ( 1 <= i & i <= len p & p0 /. i = s ) ; :: thesis: |(s,u4)| = 0
len p < (len p) + 1 by XREAL_1:31;
then A89: i < len q by A86, A88, XXREAL_0:2;
defpred S₂[ Nat] means for s2, u2 being Element of REAL n
for k being Nat st u2 = q /. $1 & 1 <= k & k < $1 & $1 <= (len p) + 1 & p0 /. k = s2 holds
|(s2,u2)| = 0 ;
A90: S₂[ 0 ] ;
A91: for k being Nat st S₂[k] holds
S₂[k + 1]

proof

let k be Nat; :: thesis: ( S₂[k] implies S₂[k + 1] )
assume A92: S₂[k] ; :: thesis: S₂[k + 1]
for s2, u2 being Element of REAL n
for k2 being Nat st u2 = q /. (k + 1) & 1 <= k2 & k2 < k + 1 & k + 1 <= (len p) + 1 & p0 /. k2 = s2 holds
|(s2,u2)| = 0

proof

let s2, u2 be Element of REAL n; :: thesis: for k2 being Nat st u2 = q /. (k + 1) & 1 <= k2 & k2 < k + 1 & k + 1 <= (len p) + 1 & p0 /. k2 = s2 holds
|(s2,u2)| = 0
let k2 be Nat; :: thesis: ( u2 = q /. (k + 1) & 1 <= k2 & k2 < k + 1 & k + 1 <= (len p) + 1 & p0 /. k2 = s2 implies |(s2,u2)| = 0 )
assume A93: ( u2 = q /. (k + 1) & 1 <= k2 & k2 < k + 1 & k + 1 <= (len p) + 1 & p0 /. k2 = s2 ) ; :: thesis: |(s2,u2)| = 0
A94: k < k + 1 by XREAL_1:31;
A95: k2 <= k by A93, NAT_1:13;

per cases ( k = 0 or k <> 0 ) ;

suppose k = 0 ; :: thesis: |(s2,u2)| = 0

hence |(s2,u2)| = 0 by A93; :: thesis: verum

end;

suppose k <> 0 ; :: thesis: |(s2,u2)| = 0

then A96: 0 + 1 <= k by NAT_1:13;
reconsider s1 = p0 /. k as Element of REAL n ;
reconsider a = q /. k, b = p0 /. k as Element of REAL n ;
A97: ( 1 <= k & k < (len p) + 1 & a = q /. k & b = p0 /. k ) by A93, A94, A96, XXREAL_0:2;
then A98: ( q /. (k + 1) <> 0* n & q . (k + 1) = (q /. k) - (|(a,b)| * (p0 /. k)) ) by A86;
1 <= k + 1 by A93, XXREAL_0:2;
then u2 = q . (k + 1) by A93, A86, FINSEQ_4:24;
then A99: |(s2,u2)| = |(s2,a)| - |(s2,(|(a,b)| * b))| by A98, EUCLID_4:31
.= |(s2,a)| - (|(a,b)| * |(s2,b)|) by EUCLID_4:26 ;
A100: k <= len p by A97, NAT_1:13;

per cases ( k2 < k or k2 = k ) by A95, XXREAL_0:1;

suppose A101: k2 < k ; :: thesis: |(s2,u2)| = 0

then A102: ( a = q /. k & 1 <= k2 & k2 < k & k < (len p) + 1 & p0 /. k2 = s2 ) by A93, A94, XXREAL_0:2;
A103: k2 < len p by A100, A101, XXREAL_0:2;
then A104: p0 /. k2 = p0 . k2 by A93, FINSEQ_4:24;
k2 in Seg (len p0) by A93, A103, FINSEQ_1:3;
then A105: k2 in dom p0 by FINSEQ_1:def 3;
then A106: s2 in rng p by A93, A104, FUNCT_1:def 5;
A107: 1 < k by A93, A101, XXREAL_0:2;
then A108: p0 /. k = p0 . k by A100, FINSEQ_4:24;
k in Seg (len p0) by A107, A100, FINSEQ_1:3;
then A109: k in dom p0 by FINSEQ_1:def 3;
then A110: b in D by A12, A108, FUNCT_1:def 5;
s2 <> b by A12, A93, A101, A104, A105, A108, A109, FUNCT_1:def 8;
then |(s2,b)| = 0 by A12, A106, A110, Def4;
hence |(s2,u2)| = 0 by A92, A99, A102; :: thesis: verum

end;

suppose A111: k2 = k ; :: thesis: |(s2,u2)| = 0

k in Seg (len p0) by A96, A100, FINSEQ_1:3;
then A112: k in dom p0 by FINSEQ_1:def 3;
p0 /. k = p0 . k by A96, A100, FINSEQ_4:24;
then b in rng p0 by A112, FUNCT_1:def 5;
then |.b.| = 1 by A12, Def5;
then |.b.| ^2 = 1 ;
hence |(s2,u2)| = |(b,a)| - (|(a,b)| * 1) by A93, A99, A111, EUCLID_2:12
.= 0 ;
:: thesis: verum

end;

end;

end;

end;

end;

hence S₂[k + 1] ; :: thesis: verum

end;

for k being Nat holds S₂[k] from NAT_1:sch 2(A90, A91);
hence |(s,u4)| = 0 by A86, A88, A89; :: thesis: verum

end;

reconsider B2 = B as finite set by A4, A7;
reconsider a2 = q /. ((len p) -' 1), b2 = p0 /. ((len p) -' 1) as Element of REAL n ;
set aq = q /. (len p);
set bq = p0 /. (len p);
A113: ( q /. (len p) = q /. (len p) & p0 /. (len p) = p0 /. (len p) ) ;
len p < (len p) + 1 by XREAL_1:31;
then A114: |.u4.| <> 0 by A13, A86, A113, EUCLID:11;
A115: abs (1 / |.u4.|) = 1 / |.u4.| by ABSVALUE:def 1;
set u0 = (1 / |.u4.|) * u4;
A116: |.((1 / |.u4.|) * u4).| = (abs (1 / |.u4.|)) * |.u4.| by EUCLID:14
.= 1 by A114, A115, XCMPLX_1:107 ;
A117: for i being Nat
for s being Element of REAL n st 1 <= i & i <= len p & p0 /. i = s holds
|(s,((1 / |.u4.|) * u4))| = 0

proof

let i be Nat; :: thesis: for s being Element of REAL n st 1 <= i & i <= len p & p0 /. i = s holds
|(s,((1 / |.u4.|) * u4))| = 0
let s be Element of REAL n; :: thesis: ( 1 <= i & i <= len p & p0 /. i = s implies |(s,((1 / |.u4.|) * u4))| = 0 )
assume A118: ( 1 <= i & i <= len p & p0 /. i = s ) ; :: thesis: |(s,((1 / |.u4.|) * u4))| = 0
A119: |(s,((1 / |.u4.|) * u4))| = (1 / |.u4.|) * |(s,u4)| by EUCLID_4:27;
|(s,u4)| = 0 by A118, A87;
hence |(s,((1 / |.u4.|) * u4))| = 0 by A119; :: thesis: verum

end;

reconsider B3 = B \/ {((1 / |.u4.|) * u4)} as Subset of (REAL n) by XBOOLE_1:8;
for x, y being real-valued FinSequence st x in B3 & y in B3 & x <> y holds
|(x,y)| = 0

proof

let x, y be real-valued FinSequence; :: thesis: ( x in B3 & y in B3 & x <> y implies |(x,y)| = 0 )
assume A120: ( x in B3 & y in B3 & x <> y ) ; :: thesis: |(x,y)| = 0

per cases ( ( x in B & y in B ) or ( x in B & y in {((1 / |.u4.|) * u4)} ) or ( x in {((1 / |.u4.|) * u4)} & y in B ) or ( x in {((1 / |.u4.|) * u4)} & y in {((1 / |.u4.|) * u4)} ) ) by A120, XBOOLE_0:def 3;

suppose ( x in B & y in B ) ; :: thesis: |(x,y)| = 0

hence |(x,y)| = 0 by A120, Def4; :: thesis: verum

end;

suppose A121: ( x in B & y in {((1 / |.u4.|) * u4)} ) ; :: thesis: |(x,y)| = 0

then A122: ( x in B & y = (1 / |.u4.|) * u4 ) by TARSKI:def 1;
consider x3 being set such that
A123: ( x3 in dom p0 & x = p0 . x3 ) by A12, A121, FUNCT_1:def 5;
A124: x3 in Seg (len p0) by A123, FINSEQ_1:def 3;
reconsider j = x3 as Element of NAT by A123;
A125: ( 1 <= j & j <= len p0 ) by A124, FINSEQ_1:3;
then p0 . x3 = p0 /. j by FINSEQ_4:24;
hence |(x,y)| = 0 by A117, A122, A123, A125; :: thesis: verum

end;

suppose A126: ( x in {((1 / |.u4.|) * u4)} & y in B ) ; :: thesis: |(x,y)| = 0

then A127: ( y in B & x = (1 / |.u4.|) * u4 ) by TARSKI:def 1;
consider y3 being set such that
A128: ( y3 in dom p0 & y = p0 . y3 ) by A12, A126, FUNCT_1:def 5;
A129: y3 in Seg (len p0) by A128, FINSEQ_1:def 3;
reconsider j = y3 as Element of NAT by A128;
A130: ( 1 <= j & j <= len p0 ) by A129, FINSEQ_1:3;
then p0 . y3 = p0 /. j by FINSEQ_4:24;
hence |(x,y)| = 0 by A117, A127, A128, A130; :: thesis: verum

end;

suppose ( x in {((1 / |.u4.|) * u4)} & y in {((1 / |.u4.|) * u4)} ) ; :: thesis: |(x,y)| = 0

then ( x in {((1 / |.u4.|) * u4)} & y = (1 / |.u4.|) * u4 ) by TARSKI:def 1;
hence |(x,y)| = 0 by A120, TARSKI:def 1; :: thesis: verum

end;

end;

end;

then A131: B3 is R-orthogonal by Def4;
B3 is R-normal by A116, Th20;
then A132: D0 = B3 by A3, A131, XBOOLE_1:7;
(1 / |.u4.|) * u4 in {((1 / |.u4.|) * u4)} by TARSKI:def 1;
then (1 / |.u4.|) * u4 in B by A132, XBOOLE_0:def 3;
then consider x3 being set such that
A133: ( x3 in dom p0 & (1 / |.u4.|) * u4 = p0 . x3 ) by A12, FUNCT_1:def 5;
A134: x3 in Seg (len p0) by A133, FINSEQ_1:def 3;
reconsider j = x3 as Element of NAT by A133;
A135: ( 1 <= j & j <= len p0 ) by A134, FINSEQ_1:3;
then p0 . x3 = p0 /. j by FINSEQ_4:24;
then |(((1 / |.u4.|) * u4),((1 / |.u4.|) * u4))| = 0 by A117, A133, A135;
hence B is Basis of RealVectSpace (Seg n) by A116, EUCLID_4:21; :: thesis: verum

end;

hence D is Basis of RealVectSpace (Seg n) by A8; :: thesis: verum

end;

end;