defpred S_{1}[ Nat] means for x being Point of (REAL-NS $1)

for xs being Element of REAL $1

for seq being sequence of (REAL-NS $1)

for xseq being sequence of (REAL $1) st xs = x & xseq = seq holds

( ( seq is convergent & lim seq = x ) iff for i being Nat st i in Seg $1 holds

ex rseqi being Real_Sequence st

for k being Nat holds

( rseqi . k = (xseq . k) . i & rseqi is convergent & xs . i = lim rseqi ) );

_{1}[ 0 ]
_{1}[n]
from NAT_1:sch 2(A55, A1); :: thesis: verum

for xs being Element of REAL $1

for seq being sequence of (REAL-NS $1)

for xseq being sequence of (REAL $1) st xs = x & xseq = seq holds

( ( seq is convergent & lim seq = x ) iff for i being Nat st i in Seg $1 holds

ex rseqi being Real_Sequence st

for k being Nat holds

( rseqi . k = (xseq . k) . i & rseqi is convergent & xs . i = lim rseqi ) );

A1: now :: thesis: for n being Nat st S_{1}[n] holds

S_{1}[n + 1]

A55:
SS

let n be Nat; :: thesis: ( S_{1}[n] implies S_{1}[n + 1] )

assume A2: S_{1}[n]
; :: thesis: S_{1}[n + 1]

_{1}[n + 1]
; :: thesis: verum

end;assume A2: S

now :: thesis: for x being Point of (REAL-NS (n + 1))

for xs being Element of REAL (n + 1)

for seq being sequence of (REAL-NS (n + 1))

for xseq being sequence of (REAL (n + 1)) st xs = x & xseq = seq holds

( ( seq is convergent & lim seq = x ) iff for i being Nat st i in Seg (n + 1) holds

ex rseqi being Real_Sequence st

for k being Nat holds

( rseqi . k = (xseq . k) . i & rseqi is convergent & xs . i = lim rseqi ) )

hence
Sfor xs being Element of REAL (n + 1)

for seq being sequence of (REAL-NS (n + 1))

for xseq being sequence of (REAL (n + 1)) st xs = x & xseq = seq holds

( ( seq is convergent & lim seq = x ) iff for i being Nat st i in Seg (n + 1) holds

ex rseqi being Real_Sequence st

for k being Nat holds

( rseqi . k = (xseq . k) . i & rseqi is convergent & xs . i = lim rseqi ) )

let x be Point of (REAL-NS (n + 1)); :: thesis: for xs being Element of REAL (n + 1)

for seq being sequence of (REAL-NS (n + 1))

for xseq being sequence of (REAL (n + 1)) st xs = x & xseq = seq holds

( ( seq is convergent & lim seq = x ) iff for i being Nat st i in Seg (n + 1) holds

ex rseqi being Real_Sequence st

for k being Nat holds

( rseqi . k = (xseq . k) . i & rseqi is convergent & xs . i = lim rseqi ) )

let xs be Element of REAL (n + 1); :: thesis: for seq being sequence of (REAL-NS (n + 1))

for xseq being sequence of (REAL (n + 1)) st xs = x & xseq = seq holds

( ( seq is convergent & lim seq = x ) iff for i being Nat st i in Seg (n + 1) holds

ex rseqi being Real_Sequence st

for k being Nat holds

( rseqi . k = (xseq . k) . i & rseqi is convergent & xs . i = lim rseqi ) )

let seq be sequence of (REAL-NS (n + 1)); :: thesis: for xseq being sequence of (REAL (n + 1)) st xs = x & xseq = seq holds

( ( seq is convergent & lim seq = x ) iff for i being Nat st i in Seg (n + 1) holds

ex rseqi being Real_Sequence st

for k being Nat holds

( rseqi . k = (xseq . k) . i & rseqi is convergent & xs . i = lim rseqi ) )

let xseq be sequence of (REAL (n + 1)); :: thesis: ( xs = x & xseq = seq implies ( ( seq is convergent & lim seq = x ) iff for i being Nat st i in Seg (n + 1) holds

ex rseqi being Real_Sequence st

for k being Nat holds

( rseqi . k = (xseq . k) . i & rseqi is convergent & xs . i = lim rseqi ) ) )

assume A3: ( xs = x & xseq = seq ) ; :: thesis: ( ( seq is convergent & lim seq = x ) iff for i being Nat st i in Seg (n + 1) holds

ex rseqi being Real_Sequence st

for k being Nat holds

( rseqi . k = (xseq . k) . i & rseqi is convergent & xs . i = lim rseqi ) )

ex rseqi being Real_Sequence st

for k being Nat holds

( rseqi . k = (xseq . k) . i & rseqi is convergent & xs . i = lim rseqi ) ) by A4; :: thesis: verum

end;for seq being sequence of (REAL-NS (n + 1))

for xseq being sequence of (REAL (n + 1)) st xs = x & xseq = seq holds

( ( seq is convergent & lim seq = x ) iff for i being Nat st i in Seg (n + 1) holds

ex rseqi being Real_Sequence st

for k being Nat holds

( rseqi . k = (xseq . k) . i & rseqi is convergent & xs . i = lim rseqi ) )

let xs be Element of REAL (n + 1); :: thesis: for seq being sequence of (REAL-NS (n + 1))

for xseq being sequence of (REAL (n + 1)) st xs = x & xseq = seq holds

( ( seq is convergent & lim seq = x ) iff for i being Nat st i in Seg (n + 1) holds

ex rseqi being Real_Sequence st

for k being Nat holds

( rseqi . k = (xseq . k) . i & rseqi is convergent & xs . i = lim rseqi ) )

let seq be sequence of (REAL-NS (n + 1)); :: thesis: for xseq being sequence of (REAL (n + 1)) st xs = x & xseq = seq holds

( ( seq is convergent & lim seq = x ) iff for i being Nat st i in Seg (n + 1) holds

ex rseqi being Real_Sequence st

for k being Nat holds

( rseqi . k = (xseq . k) . i & rseqi is convergent & xs . i = lim rseqi ) )

let xseq be sequence of (REAL (n + 1)); :: thesis: ( xs = x & xseq = seq implies ( ( seq is convergent & lim seq = x ) iff for i being Nat st i in Seg (n + 1) holds

ex rseqi being Real_Sequence st

for k being Nat holds

( rseqi . k = (xseq . k) . i & rseqi is convergent & xs . i = lim rseqi ) ) )

assume A3: ( xs = x & xseq = seq ) ; :: thesis: ( ( seq is convergent & lim seq = x ) iff for i being Nat st i in Seg (n + 1) holds

ex rseqi being Real_Sequence st

for k being Nat holds

( rseqi . k = (xseq . k) . i & rseqi is convergent & xs . i = lim rseqi ) )

A4: now :: thesis: ( ( for i being Nat st i in Seg (n + 1) holds

ex rseqi being Real_Sequence st

for k being Nat holds

( rseqi . k = (xseq . k) . i & rseqi is convergent & xs . i = lim rseqi ) ) implies ( seq is convergent & lim seq = x ) )

ex rseqi being Real_Sequence st

for k being Nat holds

( rseqi . k = (xseq . k) . i & rseqi is convergent & xs . i = lim rseqi ) ) implies ( seq is convergent & lim seq = x ) )

assume A5:
for i being Nat st i in Seg (n + 1) holds

ex rseqi being Real_Sequence st

for k being Nat holds

( rseqi . k = (xseq . k) . i & rseqi is convergent & xs . i = lim rseqi ) ; :: thesis: ( seq is convergent & lim seq = x )

thus ( seq is convergent & lim seq = x ) :: thesis: verum

end;ex rseqi being Real_Sequence st

for k being Nat holds

( rseqi . k = (xseq . k) . i & rseqi is convergent & xs . i = lim rseqi ) ; :: thesis: ( seq is convergent & lim seq = x )

thus ( seq is convergent & lim seq = x ) :: thesis: verum

proof

len xs = n + 1
by CARD_1:def 7;

then len (xs | n) = n by FINSEQ_1:59, NAT_1:11;

then dom (xs | n) = Seg n by FINSEQ_1:def 3;

then reconsider xsn = xs | n as Element of REAL n by Th6;

reconsider xn = xsn as Point of (REAL-NS n) by Def4;

defpred S_{2}[ Nat, Element of REAL n] means $2 = (xseq . $1) | n;

set seq2 = ||.(seq - x).|| (#) ||.(seq - x).||;

consider rseqn1 being Real_Sequence such that

A6: for k being Nat holds

( rseqn1 . k = (xseq . k) . (n + 1) & rseqn1 is convergent & xs . (n + 1) = lim rseqn1 ) by A5, FINSEQ_1:4;

A7: for i being Element of NAT ex y being Element of REAL n st S_{2}[i,y]

A8: for i being Element of NAT holds S_{2}[i,xseqn . i]
from FUNCT_2:sch 3(A7);

reconsider seqn = xseqn as sequence of (REAL-NS n) by Def4;

set seqn2 = ||.(seqn - xn).|| (#) ||.(seqn - xn).||;

deffunc H_{1}( Nat) -> object = |.((rseqn1 . $1) - (xs . (n + 1))).|;

consider absrseq being Real_Sequence such that

A9: for i being Nat holds absrseq . i = H_{1}(i)
from SEQ_1:sch 1();

A10: for i being Nat st i in Seg n holds

ex rseqi being Real_Sequence st

for k being Nat holds

( rseqi . k = (xseqn . k) . i & rseqi is convergent & xsn . i = lim rseqi )

set rseqn2 = absrseq (#) absrseq;

xsn = xn ;

then A16: seqn is convergent by A2, A10;

then A17: ||.(seqn - xn).|| is convergent by A15, NORMSP_1:24;

then A18: ||.(seqn - xn).|| (#) ||.(seqn - xn).|| is convergent by SEQ_2:14;

then lim absrseq = 0 by A33, SEQ_2:def 7;

then A36: lim (absrseq (#) absrseq) = 0 * 0 by A35, SEQ_2:15

.= 0 ;

A37: absrseq (#) absrseq is convergent by A35, SEQ_2:14;

then A38: ||.(seq - x).|| (#) ||.(seq - x).|| is convergent by A18, A32, SEQ_2:5;

lim ||.(seqn - xn).|| = 0 by A16, A15, NORMSP_1:24;

then lim (||.(seqn - xn).|| (#) ||.(seqn - xn).||) = 0 * 0 by A17, SEQ_2:15

.= 0 ;

then A39: lim (||.(seq - x).|| (#) ||.(seq - x).||) = 0 + 0 by A18, A37, A36, A32, SEQ_2:6

.= 0 ;

A40: for e being Real st e > 0 holds

ex m being Nat st

for k being Nat st k >= m holds

||.((seq . k) - x).|| < e

hence ( seq is convergent & lim seq = x ) by A40, NORMSP_1:def 7; :: thesis: verum

end;then len (xs | n) = n by FINSEQ_1:59, NAT_1:11;

then dom (xs | n) = Seg n by FINSEQ_1:def 3;

then reconsider xsn = xs | n as Element of REAL n by Th6;

reconsider xn = xsn as Point of (REAL-NS n) by Def4;

defpred S

set seq2 = ||.(seq - x).|| (#) ||.(seq - x).||;

consider rseqn1 being Real_Sequence such that

A6: for k being Nat holds

( rseqn1 . k = (xseq . k) . (n + 1) & rseqn1 is convergent & xs . (n + 1) = lim rseqn1 ) by A5, FINSEQ_1:4;

A7: for i being Element of NAT ex y being Element of REAL n st S

proof

consider xseqn being sequence of (REAL n) such that
let i be Element of NAT ; :: thesis: ex y being Element of REAL n st S_{2}[i,y]

take y = (xseq . i) | n; :: thesis: ( y is Element of REAL n & S_{2}[i,y] )

len (xseq . i) = n + 1 by CARD_1:def 7;

then len ((xseq . i) | n) = n by FINSEQ_1:59, NAT_1:11;

then dom ((xseq . i) | n) = Seg n by FINSEQ_1:def 3;

hence ( y is Element of REAL n & S_{2}[i,y] )
by Th6; :: thesis: verum

end;take y = (xseq . i) | n; :: thesis: ( y is Element of REAL n & S

len (xseq . i) = n + 1 by CARD_1:def 7;

then len ((xseq . i) | n) = n by FINSEQ_1:59, NAT_1:11;

then dom ((xseq . i) | n) = Seg n by FINSEQ_1:def 3;

hence ( y is Element of REAL n & S

A8: for i being Element of NAT holds S

reconsider seqn = xseqn as sequence of (REAL-NS n) by Def4;

set seqn2 = ||.(seqn - xn).|| (#) ||.(seqn - xn).||;

deffunc H

consider absrseq being Real_Sequence such that

A9: for i being Nat holds absrseq . i = H

A10: for i being Nat st i in Seg n holds

ex rseqi being Real_Sequence st

for k being Nat holds

( rseqi . k = (xseqn . k) . i & rseqi is convergent & xsn . i = lim rseqi )

proof

then A15:
xn = lim seqn
by A2;
let i be Nat; :: thesis: ( i in Seg n implies ex rseqi being Real_Sequence st

for k being Nat holds

( rseqi . k = (xseqn . k) . i & rseqi is convergent & xsn . i = lim rseqi ) )

assume A11: i in Seg n ; :: thesis: ex rseqi being Real_Sequence st

for k being Nat holds

( rseqi . k = (xseqn . k) . i & rseqi is convergent & xsn . i = lim rseqi )

n <= n + 1 by NAT_1:11;

then Seg n c= Seg (n + 1) by FINSEQ_1:5;

then consider rseqi being Real_Sequence such that

A12: for k being Nat holds

( rseqi . k = (xseq . k) . i & rseqi is convergent & xs . i = lim rseqi ) by A5, A11;

.= xs . i by A11, FUNCT_1:49 ;

hence ex rseqi being Real_Sequence st

for k being Nat holds

( rseqi . k = (xseqn . k) . i & rseqi is convergent & xsn . i = lim rseqi ) by A12, A13; :: thesis: verum

end;for k being Nat holds

( rseqi . k = (xseqn . k) . i & rseqi is convergent & xsn . i = lim rseqi ) )

assume A11: i in Seg n ; :: thesis: ex rseqi being Real_Sequence st

for k being Nat holds

( rseqi . k = (xseqn . k) . i & rseqi is convergent & xsn . i = lim rseqi )

n <= n + 1 by NAT_1:11;

then Seg n c= Seg (n + 1) by FINSEQ_1:5;

then consider rseqi being Real_Sequence such that

A12: for k being Nat holds

( rseqi . k = (xseq . k) . i & rseqi is convergent & xs . i = lim rseqi ) by A5, A11;

A13: now :: thesis: for k being Nat holds rseqi . k = (xseqn . k) . i

xsn . i =
(xs | (Seg n)) . i
by FINSEQ_1:def 15
let k be Nat; :: thesis: rseqi . k = (xseqn . k) . i

A14: k in NAT by ORDINAL1:def 12;

thus rseqi . k = (xseq . k) . i by A12

.= ((xseq . k) | (Seg n)) . i by A11, FUNCT_1:49

.= ((xseq . k) | n) . i by FINSEQ_1:def 15

.= (xseqn . k) . i by A8, A14 ; :: thesis: verum

end;A14: k in NAT by ORDINAL1:def 12;

thus rseqi . k = (xseq . k) . i by A12

.= ((xseq . k) | (Seg n)) . i by A11, FUNCT_1:49

.= ((xseq . k) | n) . i by FINSEQ_1:def 15

.= (xseqn . k) . i by A8, A14 ; :: thesis: verum

.= xs . i by A11, FUNCT_1:49 ;

hence ex rseqi being Real_Sequence st

for k being Nat holds

( rseqi . k = (xseqn . k) . i & rseqi is convergent & xsn . i = lim rseqi ) by A12, A13; :: thesis: verum

set rseqn2 = absrseq (#) absrseq;

xsn = xn ;

then A16: seqn is convergent by A2, A10;

then A17: ||.(seqn - xn).|| is convergent by A15, NORMSP_1:24;

then A18: ||.(seqn - xn).|| (#) ||.(seqn - xn).|| is convergent by SEQ_2:14;

now :: thesis: for k being Nat holds (||.(seq - x).|| (#) ||.(seq - x).||) . k = ((||.(seqn - xn).|| (#) ||.(seqn - xn).||) . k) + ((absrseq (#) absrseq) . k)

then A32:
||.(seq - x).|| (#) ||.(seq - x).|| = (||.(seqn - xn).|| (#) ||.(seqn - xn).||) + (absrseq (#) absrseq)
by SEQ_1:7;reconsider rxs = xs as Element of (n + 1) -tuples_on REAL by EUCLID:def 1;

let k be Nat; :: thesis: (||.(seq - x).|| (#) ||.(seq - x).||) . k = ((||.(seqn - xn).|| (#) ||.(seqn - xn).||) . k) + ((absrseq (#) absrseq) . k)

A19: k in NAT by ORDINAL1:def 12;

A20: ||.(seq - x).|| . k = ||.((seq - x) . k).|| by NORMSP_0:def 4

.= ||.((seq . k) - x).|| by NORMSP_1:def 4 ;

reconsider rxseqk = xseq . k as Element of (n + 1) -tuples_on REAL by EUCLID:def 1;

A21: ||.(seqn - xn).|| . k = ||.((seqn - xn) . k).|| by NORMSP_0:def 4

.= ||.((seqn . k) - xn).|| by NORMSP_1:def 4 ;

len ((xseqn . k) - xsn) = n by CARD_1:def 7;

then A22: dom ((xseqn . k) - xsn) = Seg n by FINSEQ_1:def 3;

A23: ((xseq . k) - xs) . (n + 1) = (rxseqk . (n + 1)) - (rxs . (n + 1)) by RVSUM_1:27

.= (rseqn1 . k) - (xs . (n + 1)) by A6 ;

len ((xseq . k) - xs) = n + 1 by CARD_1:def 7;

then A24: len (((xseq . k) - xs) | n) = n by FINSEQ_1:59, NAT_1:11;

then A29: ((xseq . k) - xs) | n = (xseqn . k) - xsn by A22, A25, FINSEQ_1:13;

A30: 0 <= ((rseqn1 . k) - (xs . (n + 1))) ^2 by XREAL_1:63;

A31: absrseq . k = |.((rseqn1 . k) - (xs . (n + 1))).| by A9;

||.((seq . k) - x).|| = |.((xseq . k) - xs).| by A3, Th1, Th5;

hence (||.(seq - x).|| (#) ||.(seq - x).||) . k = |.((xseq . k) - xs).| ^2 by A20, SEQ_1:8

.= (|.((xseqn . k) - xsn).| ^2) + (((rseqn1 . k) - (xs . (n + 1))) ^2) by A23, A29, Th10

.= (||.((seqn . k) - xn).|| ^2) + (((rseqn1 . k) - (xs . (n + 1))) ^2) by Th1, Th5

.= ((||.(seqn - xn).|| (#) ||.(seqn - xn).||) . k) + (((rseqn1 . k) - (xs . (n + 1))) ^2) by A21, SEQ_1:8

.= ((||.(seqn - xn).|| (#) ||.(seqn - xn).||) . k) + |.(((rseqn1 . k) - (xs . (n + 1))) * ((rseqn1 . k) - (xs . (n + 1)))).| by A30, ABSVALUE:def 1

.= ((||.(seqn - xn).|| (#) ||.(seqn - xn).||) . k) + (|.((rseqn1 . k) - (xs . (n + 1))).| * |.((rseqn1 . k) - (xs . (n + 1))).|) by COMPLEX1:65

.= ((||.(seqn - xn).|| (#) ||.(seqn - xn).||) . k) + ((absrseq (#) absrseq) . k) by A31, SEQ_1:8 ;

:: thesis: verum

end;let k be Nat; :: thesis: (||.(seq - x).|| (#) ||.(seq - x).||) . k = ((||.(seqn - xn).|| (#) ||.(seqn - xn).||) . k) + ((absrseq (#) absrseq) . k)

A19: k in NAT by ORDINAL1:def 12;

A20: ||.(seq - x).|| . k = ||.((seq - x) . k).|| by NORMSP_0:def 4

.= ||.((seq . k) - x).|| by NORMSP_1:def 4 ;

reconsider rxseqk = xseq . k as Element of (n + 1) -tuples_on REAL by EUCLID:def 1;

A21: ||.(seqn - xn).|| . k = ||.((seqn - xn) . k).|| by NORMSP_0:def 4

.= ||.((seqn . k) - xn).|| by NORMSP_1:def 4 ;

len ((xseqn . k) - xsn) = n by CARD_1:def 7;

then A22: dom ((xseqn . k) - xsn) = Seg n by FINSEQ_1:def 3;

A23: ((xseq . k) - xs) . (n + 1) = (rxseqk . (n + 1)) - (rxs . (n + 1)) by RVSUM_1:27

.= (rseqn1 . k) - (xs . (n + 1)) by A6 ;

len ((xseq . k) - xs) = n + 1 by CARD_1:def 7;

then A24: len (((xseq . k) - xs) | n) = n by FINSEQ_1:59, NAT_1:11;

A25: now :: thesis: for i being Nat st i in dom (((xseq . k) - xs) | n) holds

(((xseq . k) - xs) | n) . i = ((xseqn . k) - xsn) . i

dom (((xseq . k) - xs) | n) = Seg n
by A24, FINSEQ_1:def 3;(((xseq . k) - xs) | n) . i = ((xseqn . k) - xsn) . i

reconsider xseq2 = xseqn . k, xs2 = xsn as Element of n -tuples_on REAL by EUCLID:def 1;

reconsider xseq1 = xseq . k, xs1 = xs as Element of (n + 1) -tuples_on REAL by EUCLID:def 1;

let i be Nat; :: thesis: ( i in dom (((xseq . k) - xs) | n) implies (((xseq . k) - xs) | n) . i = ((xseqn . k) - xsn) . i )

assume i in dom (((xseq . k) - xs) | n) ; :: thesis: (((xseq . k) - xs) | n) . i = ((xseqn . k) - xsn) . i

then A26: i in Seg n by A24, FINSEQ_1:def 3;

A27: ((xseqn . k) - xsn) . i = (xseq2 . i) - (xs2 . i) by RVSUM_1:27;

A28: ((xseq . k) - xs) . i = (xseq1 . i) - (xs1 . i) by RVSUM_1:27;

thus (((xseq . k) - xs) | n) . i = (((xseq . k) - xs) | (Seg n)) . i by FINSEQ_1:def 15

.= ((xseq . k) - xs) . i by A26, FUNCT_1:49

.= (((xseq . k) | (Seg n)) . i) - (xs . i) by A26, A28, FUNCT_1:49

.= (((xseq . k) | (Seg n)) . i) - ((xs | (Seg n)) . i) by A26, FUNCT_1:49

.= (((xseq . k) | n) . i) - ((xs | (Seg n)) . i) by FINSEQ_1:def 15

.= (((xseq . k) | n) . i) - ((xs | n) . i) by FINSEQ_1:def 15

.= ((xseqn . k) - xsn) . i by A8, A27, A19 ; :: thesis: verum

end;reconsider xseq1 = xseq . k, xs1 = xs as Element of (n + 1) -tuples_on REAL by EUCLID:def 1;

let i be Nat; :: thesis: ( i in dom (((xseq . k) - xs) | n) implies (((xseq . k) - xs) | n) . i = ((xseqn . k) - xsn) . i )

assume i in dom (((xseq . k) - xs) | n) ; :: thesis: (((xseq . k) - xs) | n) . i = ((xseqn . k) - xsn) . i

then A26: i in Seg n by A24, FINSEQ_1:def 3;

A27: ((xseqn . k) - xsn) . i = (xseq2 . i) - (xs2 . i) by RVSUM_1:27;

A28: ((xseq . k) - xs) . i = (xseq1 . i) - (xs1 . i) by RVSUM_1:27;

thus (((xseq . k) - xs) | n) . i = (((xseq . k) - xs) | (Seg n)) . i by FINSEQ_1:def 15

.= ((xseq . k) - xs) . i by A26, FUNCT_1:49

.= (((xseq . k) | (Seg n)) . i) - (xs . i) by A26, A28, FUNCT_1:49

.= (((xseq . k) | (Seg n)) . i) - ((xs | (Seg n)) . i) by A26, FUNCT_1:49

.= (((xseq . k) | n) . i) - ((xs | (Seg n)) . i) by FINSEQ_1:def 15

.= (((xseq . k) | n) . i) - ((xs | n) . i) by FINSEQ_1:def 15

.= ((xseqn . k) - xsn) . i by A8, A27, A19 ; :: thesis: verum

then A29: ((xseq . k) - xs) | n = (xseqn . k) - xsn by A22, A25, FINSEQ_1:13;

A30: 0 <= ((rseqn1 . k) - (xs . (n + 1))) ^2 by XREAL_1:63;

A31: absrseq . k = |.((rseqn1 . k) - (xs . (n + 1))).| by A9;

||.((seq . k) - x).|| = |.((xseq . k) - xs).| by A3, Th1, Th5;

hence (||.(seq - x).|| (#) ||.(seq - x).||) . k = |.((xseq . k) - xs).| ^2 by A20, SEQ_1:8

.= (|.((xseqn . k) - xsn).| ^2) + (((rseqn1 . k) - (xs . (n + 1))) ^2) by A23, A29, Th10

.= (||.((seqn . k) - xn).|| ^2) + (((rseqn1 . k) - (xs . (n + 1))) ^2) by Th1, Th5

.= ((||.(seqn - xn).|| (#) ||.(seqn - xn).||) . k) + (((rseqn1 . k) - (xs . (n + 1))) ^2) by A21, SEQ_1:8

.= ((||.(seqn - xn).|| (#) ||.(seqn - xn).||) . k) + |.(((rseqn1 . k) - (xs . (n + 1))) * ((rseqn1 . k) - (xs . (n + 1)))).| by A30, ABSVALUE:def 1

.= ((||.(seqn - xn).|| (#) ||.(seqn - xn).||) . k) + (|.((rseqn1 . k) - (xs . (n + 1))).| * |.((rseqn1 . k) - (xs . (n + 1))).|) by COMPLEX1:65

.= ((||.(seqn - xn).|| (#) ||.(seqn - xn).||) . k) + ((absrseq (#) absrseq) . k) by A31, SEQ_1:8 ;

:: thesis: verum

A33: now :: thesis: for e being Real st e > 0 holds

ex m being Nat st

for k being Nat st m <= k holds

|.((absrseq . k) - 0).| < e

then A35:
absrseq is convergent
by SEQ_2:def 6;ex m being Nat st

for k being Nat st m <= k holds

|.((absrseq . k) - 0).| < e

let e be Real; :: thesis: ( e > 0 implies ex m being Nat st

for k being Nat st m <= k holds

|.((absrseq . k) - 0).| < e )

assume e > 0 ; :: thesis: ex m being Nat st

for k being Nat st m <= k holds

|.((absrseq . k) - 0).| < e

then consider m being Nat such that

A34: for k being Nat st m <= k holds

|.((rseqn1 . k) - (xs . (n + 1))).| < e by A6, SEQ_2:def 7;

for k being Nat st m <= k holds

|.((absrseq . k) - 0).| < e ; :: thesis: verum

end;for k being Nat st m <= k holds

|.((absrseq . k) - 0).| < e )

assume e > 0 ; :: thesis: ex m being Nat st

for k being Nat st m <= k holds

|.((absrseq . k) - 0).| < e

then consider m being Nat such that

A34: for k being Nat st m <= k holds

|.((rseqn1 . k) - (xs . (n + 1))).| < e by A6, SEQ_2:def 7;

now :: thesis: for k being Nat st m <= k holds

|.((absrseq . k) - 0).| < e

hence
ex m being Nat st |.((absrseq . k) - 0).| < e

let k be Nat; :: thesis: ( m <= k implies |.((absrseq . k) - 0).| < e )

assume m <= k ; :: thesis: |.((absrseq . k) - 0).| < e

then |.(|.((rseqn1 . k) - (xs . (n + 1))).| - 0).| < e by A34;

hence |.((absrseq . k) - 0).| < e by A9; :: thesis: verum

end;assume m <= k ; :: thesis: |.((absrseq . k) - 0).| < e

then |.(|.((rseqn1 . k) - (xs . (n + 1))).| - 0).| < e by A34;

hence |.((absrseq . k) - 0).| < e by A9; :: thesis: verum

for k being Nat st m <= k holds

|.((absrseq . k) - 0).| < e ; :: thesis: verum

then lim absrseq = 0 by A33, SEQ_2:def 7;

then A36: lim (absrseq (#) absrseq) = 0 * 0 by A35, SEQ_2:15

.= 0 ;

A37: absrseq (#) absrseq is convergent by A35, SEQ_2:14;

then A38: ||.(seq - x).|| (#) ||.(seq - x).|| is convergent by A18, A32, SEQ_2:5;

lim ||.(seqn - xn).|| = 0 by A16, A15, NORMSP_1:24;

then lim (||.(seqn - xn).|| (#) ||.(seqn - xn).||) = 0 * 0 by A17, SEQ_2:15

.= 0 ;

then A39: lim (||.(seq - x).|| (#) ||.(seq - x).||) = 0 + 0 by A18, A37, A36, A32, SEQ_2:6

.= 0 ;

A40: for e being Real st e > 0 holds

ex m being Nat st

for k being Nat st k >= m holds

||.((seq . k) - x).|| < e

proof

then
seq is convergent
by NORMSP_1:def 6;
let e be Real; :: thesis: ( e > 0 implies ex m being Nat st

for k being Nat st k >= m holds

||.((seq . k) - x).|| < e )

assume A41: e > 0 ; :: thesis: ex m being Nat st

for k being Nat st k >= m holds

||.((seq . k) - x).|| < e

e * 0 < e * e by A41, XREAL_1:97;

then consider m being Nat such that

A42: for k being Nat st m <= k holds

|.(((||.(seq - x).|| (#) ||.(seq - x).||) . k) - 0).| < e * e by A38, A39, SEQ_2:def 7;

for k being Nat st k >= m holds

||.((seq . k) - x).|| < e ; :: thesis: verum

end;for k being Nat st k >= m holds

||.((seq . k) - x).|| < e )

assume A41: e > 0 ; :: thesis: ex m being Nat st

for k being Nat st k >= m holds

||.((seq . k) - x).|| < e

e * 0 < e * e by A41, XREAL_1:97;

then consider m being Nat such that

A42: for k being Nat st m <= k holds

|.(((||.(seq - x).|| (#) ||.(seq - x).||) . k) - 0).| < e * e by A38, A39, SEQ_2:def 7;

now :: thesis: for k being Nat st m <= k holds

||.((seq . k) - x).|| < e

hence
ex m being Nat st ||.((seq . k) - x).|| < e

let k be Nat; :: thesis: ( m <= k implies ||.((seq . k) - x).|| < e )

assume A43: m <= k ; :: thesis: ||.((seq . k) - x).|| < e

||.(seq - x).|| . k = ||.((seq - x) . k).|| by NORMSP_0:def 4

.= ||.((seq . k) - x).|| by NORMSP_1:def 4 ;

then (||.(seq - x).|| (#) ||.(seq - x).||) . k = ||.((seq . k) - x).|| * ||.((seq . k) - x).|| by SEQ_1:8;

then |.(((||.(seq - x).|| (#) ||.(seq - x).||) . k) - 0).| = ||.((seq . k) - x).|| * ||.((seq . k) - x).|| by ABSVALUE:def 1;

then A44: ||.((seq . k) - x).|| * ||.((seq . k) - x).|| < e * e by A42, A43;

A45: sqrt (||.((seq . k) - x).|| * ||.((seq . k) - x).||) = sqrt (||.((seq . k) - x).|| ^2)

.= ||.((seq . k) - x).|| by SQUARE_1:22 ;

sqrt (e * e) = sqrt (e ^2)

.= e by A41, SQUARE_1:22 ;

hence ||.((seq . k) - x).|| < e by A44, A45, SQUARE_1:27; :: thesis: verum

end;assume A43: m <= k ; :: thesis: ||.((seq . k) - x).|| < e

||.(seq - x).|| . k = ||.((seq - x) . k).|| by NORMSP_0:def 4

.= ||.((seq . k) - x).|| by NORMSP_1:def 4 ;

then (||.(seq - x).|| (#) ||.(seq - x).||) . k = ||.((seq . k) - x).|| * ||.((seq . k) - x).|| by SEQ_1:8;

then |.(((||.(seq - x).|| (#) ||.(seq - x).||) . k) - 0).| = ||.((seq . k) - x).|| * ||.((seq . k) - x).|| by ABSVALUE:def 1;

then A44: ||.((seq . k) - x).|| * ||.((seq . k) - x).|| < e * e by A42, A43;

A45: sqrt (||.((seq . k) - x).|| * ||.((seq . k) - x).||) = sqrt (||.((seq . k) - x).|| ^2)

.= ||.((seq . k) - x).|| by SQUARE_1:22 ;

sqrt (e * e) = sqrt (e ^2)

.= e by A41, SQUARE_1:22 ;

hence ||.((seq . k) - x).|| < e by A44, A45, SQUARE_1:27; :: thesis: verum

for k being Nat st k >= m holds

||.((seq . k) - x).|| < e ; :: thesis: verum

hence ( seq is convergent & lim seq = x ) by A40, NORMSP_1:def 7; :: thesis: verum

now :: thesis: ( seq is convergent & lim seq = x implies for i being Nat st i in Seg (n + 1) holds

ex rseqi being Real_Sequence st

for k being Nat holds

( rseqi . k = (xseq . k) . i & rseqi is convergent & xs . i = lim rseqi ) )

hence
( ( seq is convergent & lim seq = x ) iff for i being Nat st i in Seg (n + 1) holds ex rseqi being Real_Sequence st

for k being Nat holds

( rseqi . k = (xseq . k) . i & rseqi is convergent & xs . i = lim rseqi ) )

assume A46:
( seq is convergent & lim seq = x )
; :: thesis: for i being Nat st i in Seg (n + 1) holds

ex rseqi being Real_Sequence st

for k being Nat holds

( rseqi . k = (xseq . k) . i & rseqi is convergent & xs . i = lim rseqi )

ex rseqi being Real_Sequence st

for k being Nat holds

( rseqi . k = (xseq . k) . i & rseqi is convergent & xs . i = lim rseqi ) ; :: thesis: verum

end;ex rseqi being Real_Sequence st

for k being Nat holds

( rseqi . k = (xseq . k) . i & rseqi is convergent & xs . i = lim rseqi )

now :: thesis: for i being Nat st i in Seg (n + 1) holds

ex rseqi being Real_Sequence st

for k being Nat holds

( rseqi . k = (xseq . k) . i & rseqi is convergent & xs . i = lim rseqi )

hence
for i being Nat st i in Seg (n + 1) holds ex rseqi being Real_Sequence st

for k being Nat holds

( rseqi . k = (xseq . k) . i & rseqi is convergent & xs . i = lim rseqi )

let i be Nat; :: thesis: ( i in Seg (n + 1) implies ex rseqi being Real_Sequence st

for k being Nat holds

( rseqi . k = (xseq . k) . i & rseqi is convergent & xs . i = lim rseqi ) )

assume A47: i in Seg (n + 1) ; :: thesis: ex rseqi being Real_Sequence st

for k being Nat holds

( rseqi . k = (xseq . k) . i & rseqi is convergent & xs . i = lim rseqi )

deffunc H_{1}( Nat) -> set = (xseq . $1) . i;

consider rseqi being Real_Sequence such that

A48: for l being Nat holds rseqi . l = H_{1}(l)
from SEQ_1:sch 1();

then xs . i = lim rseqi by A49, SEQ_2:def 7;

hence ex rseqi being Real_Sequence st

for k being Nat holds

( rseqi . k = (xseq . k) . i & rseqi is convergent & xs . i = lim rseqi ) by A48, A54; :: thesis: verum

end;for k being Nat holds

( rseqi . k = (xseq . k) . i & rseqi is convergent & xs . i = lim rseqi ) )

assume A47: i in Seg (n + 1) ; :: thesis: ex rseqi being Real_Sequence st

for k being Nat holds

( rseqi . k = (xseq . k) . i & rseqi is convergent & xs . i = lim rseqi )

deffunc H

consider rseqi being Real_Sequence such that

A48: for l being Nat holds rseqi . l = H

A49: now :: thesis: for e being Real st e > 0 holds

ex k being Nat st

for m being Nat st k <= m holds

|.((rseqi . m) - (xs . i)).| < e

then A54:
rseqi is convergent
by SEQ_2:def 6;ex k being Nat st

for m being Nat st k <= m holds

|.((rseqi . m) - (xs . i)).| < e

let e be Real; :: thesis: ( e > 0 implies ex k being Nat st

for m being Nat st k <= m holds

|.((rseqi . m) - (xs . i)).| < e )

assume A50: e > 0 ; :: thesis: ex k being Nat st

for m being Nat st k <= m holds

|.((rseqi . m) - (xs . i)).| < e

thus ex k being Nat st

for m being Nat st k <= m holds

|.((rseqi . m) - (xs . i)).| < e :: thesis: verum

end;for m being Nat st k <= m holds

|.((rseqi . m) - (xs . i)).| < e )

assume A50: e > 0 ; :: thesis: ex k being Nat st

for m being Nat st k <= m holds

|.((rseqi . m) - (xs . i)).| < e

thus ex k being Nat st

for m being Nat st k <= m holds

|.((rseqi . m) - (xs . i)).| < e :: thesis: verum

proof

consider k being Nat such that

A51: for m being Nat st m >= k holds

||.((seq . m) - x).|| < e by A46, A50, NORMSP_1:def 7;

take k ; :: thesis: for m being Nat st k <= m holds

|.((rseqi . m) - (xs . i)).| < e

let m be Nat; :: thesis: ( k <= m implies |.((rseqi . m) - (xs . i)).| < e )

assume k <= m ; :: thesis: |.((rseqi . m) - (xs . i)).| < e

then A52: ||.((seq . m) - x).|| < e by A51;

len ((xseq . m) - xs) = n + 1 by CARD_1:def 7;

then i in dom ((xseq . m) - xs) by A47, FINSEQ_1:def 3;

then ((xseq . m) . i) - (xs . i) = ((xseq . m) - xs) . i by VALUED_1:13;

then A53: |.(((xseq . m) . i) - (xs . i)).| <= ||.((seq . m) - x).|| by A3, A47, Th5, Th9;

(rseqi . m) - (xs . i) = ((xseq . m) . i) - (xs . i) by A48;

hence |.((rseqi . m) - (xs . i)).| < e by A52, A53, XXREAL_0:2; :: thesis: verum

end;A51: for m being Nat st m >= k holds

||.((seq . m) - x).|| < e by A46, A50, NORMSP_1:def 7;

take k ; :: thesis: for m being Nat st k <= m holds

|.((rseqi . m) - (xs . i)).| < e

let m be Nat; :: thesis: ( k <= m implies |.((rseqi . m) - (xs . i)).| < e )

assume k <= m ; :: thesis: |.((rseqi . m) - (xs . i)).| < e

then A52: ||.((seq . m) - x).|| < e by A51;

len ((xseq . m) - xs) = n + 1 by CARD_1:def 7;

then i in dom ((xseq . m) - xs) by A47, FINSEQ_1:def 3;

then ((xseq . m) . i) - (xs . i) = ((xseq . m) - xs) . i by VALUED_1:13;

then A53: |.(((xseq . m) . i) - (xs . i)).| <= ||.((seq . m) - x).|| by A3, A47, Th5, Th9;

(rseqi . m) - (xs . i) = ((xseq . m) . i) - (xs . i) by A48;

hence |.((rseqi . m) - (xs . i)).| < e by A52, A53, XXREAL_0:2; :: thesis: verum

then xs . i = lim rseqi by A49, SEQ_2:def 7;

hence ex rseqi being Real_Sequence st

for k being Nat holds

( rseqi . k = (xseq . k) . i & rseqi is convergent & xs . i = lim rseqi ) by A48, A54; :: thesis: verum

ex rseqi being Real_Sequence st

for k being Nat holds

( rseqi . k = (xseq . k) . i & rseqi is convergent & xs . i = lim rseqi ) ; :: thesis: verum

ex rseqi being Real_Sequence st

for k being Nat holds

( rseqi . k = (xseq . k) . i & rseqi is convergent & xs . i = lim rseqi ) ) by A4; :: thesis: verum

proof

thus
for n being Nat holds S
let x be Point of (REAL-NS 0); :: thesis: for xs being Element of REAL 0

for seq being sequence of (REAL-NS 0)

for xseq being sequence of (REAL 0) st xs = x & xseq = seq holds

( ( seq is convergent & lim seq = x ) iff for i being Nat st i in Seg 0 holds

ex rseqi being Real_Sequence st

for k being Nat holds

( rseqi . k = (xseq . k) . i & rseqi is convergent & xs . i = lim rseqi ) )

let xs be Element of REAL 0; :: thesis: for seq being sequence of (REAL-NS 0)

for xseq being sequence of (REAL 0) st xs = x & xseq = seq holds

( ( seq is convergent & lim seq = x ) iff for i being Nat st i in Seg 0 holds

ex rseqi being Real_Sequence st

for k being Nat holds

( rseqi . k = (xseq . k) . i & rseqi is convergent & xs . i = lim rseqi ) )

let seq be sequence of (REAL-NS 0); :: thesis: for xseq being sequence of (REAL 0) st xs = x & xseq = seq holds

( ( seq is convergent & lim seq = x ) iff for i being Nat st i in Seg 0 holds

ex rseqi being Real_Sequence st

for k being Nat holds

( rseqi . k = (xseq . k) . i & rseqi is convergent & xs . i = lim rseqi ) )

let xseq be sequence of (REAL 0); :: thesis: ( xs = x & xseq = seq implies ( ( seq is convergent & lim seq = x ) iff for i being Nat st i in Seg 0 holds

ex rseqi being Real_Sequence st

for k being Nat holds

( rseqi . k = (xseq . k) . i & rseqi is convergent & xs . i = lim rseqi ) ) )

assume that

A56: xs = x and

A57: xseq = seq ; :: thesis: ( ( seq is convergent & lim seq = x ) iff for i being Nat st i in Seg 0 holds

ex rseqi being Real_Sequence st

for k being Nat holds

( rseqi . k = (xseq . k) . i & rseqi is convergent & xs . i = lim rseqi ) )

ex rseqi being Real_Sequence st

for k being Nat holds

( rseqi . k = (xseq . k) . i & rseqi is convergent & xs . i = lim rseqi ) ) ; :: thesis: verum

end;for seq being sequence of (REAL-NS 0)

for xseq being sequence of (REAL 0) st xs = x & xseq = seq holds

( ( seq is convergent & lim seq = x ) iff for i being Nat st i in Seg 0 holds

ex rseqi being Real_Sequence st

for k being Nat holds

( rseqi . k = (xseq . k) . i & rseqi is convergent & xs . i = lim rseqi ) )

let xs be Element of REAL 0; :: thesis: for seq being sequence of (REAL-NS 0)

for xseq being sequence of (REAL 0) st xs = x & xseq = seq holds

( ( seq is convergent & lim seq = x ) iff for i being Nat st i in Seg 0 holds

ex rseqi being Real_Sequence st

for k being Nat holds

( rseqi . k = (xseq . k) . i & rseqi is convergent & xs . i = lim rseqi ) )

let seq be sequence of (REAL-NS 0); :: thesis: for xseq being sequence of (REAL 0) st xs = x & xseq = seq holds

( ( seq is convergent & lim seq = x ) iff for i being Nat st i in Seg 0 holds

ex rseqi being Real_Sequence st

for k being Nat holds

( rseqi . k = (xseq . k) . i & rseqi is convergent & xs . i = lim rseqi ) )

let xseq be sequence of (REAL 0); :: thesis: ( xs = x & xseq = seq implies ( ( seq is convergent & lim seq = x ) iff for i being Nat st i in Seg 0 holds

ex rseqi being Real_Sequence st

for k being Nat holds

( rseqi . k = (xseq . k) . i & rseqi is convergent & xs . i = lim rseqi ) ) )

assume that

A56: xs = x and

A57: xseq = seq ; :: thesis: ( ( seq is convergent & lim seq = x ) iff for i being Nat st i in Seg 0 holds

ex rseqi being Real_Sequence st

for k being Nat holds

( rseqi . k = (xseq . k) . i & rseqi is convergent & xs . i = lim rseqi ) )

now :: thesis: ( ( for i being Nat st i in Seg 0 holds

ex rseqi being Real_Sequence st

for k being Nat holds

( rseqi . k = (xseq . k) . i & rseqi is convergent & xs . i = lim rseqi ) ) implies ( seq is convergent & lim seq = x ) )

hence
( ( seq is convergent & lim seq = x ) iff for i being Nat st i in Seg 0 holds ex rseqi being Real_Sequence st

for k being Nat holds

( rseqi . k = (xseq . k) . i & rseqi is convergent & xs . i = lim rseqi ) ) implies ( seq is convergent & lim seq = x ) )

assume
for i being Nat st i in Seg 0 holds

ex rseqi being Real_Sequence st

for k being Nat holds

( rseqi . k = (xseq . k) . i & rseqi is convergent & xs . i = lim rseqi ) ; :: thesis: ( seq is convergent & lim seq = x )

A58: for i being Nat holds seq . i = 0. (REAL-NS 0)

then A59: x = 0. (REAL-NS 0) by A56, Def4;

A60: for r being Real st 0 < r holds

ex m being Nat st

for k being Nat st m <= k holds

||.((seq . k) - x).|| < r

hence ( seq is convergent & lim seq = x ) by A60, NORMSP_1:def 7; :: thesis: verum

end;ex rseqi being Real_Sequence st

for k being Nat holds

( rseqi . k = (xseq . k) . i & rseqi is convergent & xs . i = lim rseqi ) ; :: thesis: ( seq is convergent & lim seq = x )

A58: for i being Nat holds seq . i = 0. (REAL-NS 0)

proof

xs = 0* 0
;
let i be Nat; :: thesis: seq . i = 0. (REAL-NS 0)

xseq . i = 0.REAL 0 ;

hence seq . i = 0. (REAL-NS 0) by A57, Def4; :: thesis: verum

end;xseq . i = 0.REAL 0 ;

hence seq . i = 0. (REAL-NS 0) by A57, Def4; :: thesis: verum

then A59: x = 0. (REAL-NS 0) by A56, Def4;

A60: for r being Real st 0 < r holds

ex m being Nat st

for k being Nat st m <= k holds

||.((seq . k) - x).|| < r

proof

then
seq is convergent
by NORMSP_1:def 6;
let r be Real; :: thesis: ( 0 < r implies ex m being Nat st

for k being Nat st m <= k holds

||.((seq . k) - x).|| < r )

assume A61: 0 < r ; :: thesis: ex m being Nat st

for k being Nat st m <= k holds

||.((seq . k) - x).|| < r

take m = 1; :: thesis: for k being Nat st m <= k holds

||.((seq . k) - x).|| < r

let k be Nat; :: thesis: ( m <= k implies ||.((seq . k) - x).|| < r )

assume m <= k ; :: thesis: ||.((seq . k) - x).|| < r

||.((seq . k) - x).|| = ||.((0. (REAL-NS 0)) - (0. (REAL-NS 0))).|| by A59, A58

.= ||.(0. (REAL-NS 0)).|| by RLVECT_1:15

.= 0 ;

hence ||.((seq . k) - x).|| < r by A61; :: thesis: verum

end;for k being Nat st m <= k holds

||.((seq . k) - x).|| < r )

assume A61: 0 < r ; :: thesis: ex m being Nat st

for k being Nat st m <= k holds

||.((seq . k) - x).|| < r

take m = 1; :: thesis: for k being Nat st m <= k holds

||.((seq . k) - x).|| < r

let k be Nat; :: thesis: ( m <= k implies ||.((seq . k) - x).|| < r )

assume m <= k ; :: thesis: ||.((seq . k) - x).|| < r

||.((seq . k) - x).|| = ||.((0. (REAL-NS 0)) - (0. (REAL-NS 0))).|| by A59, A58

.= ||.(0. (REAL-NS 0)).|| by RLVECT_1:15

.= 0 ;

hence ||.((seq . k) - x).|| < r by A61; :: thesis: verum

hence ( seq is convergent & lim seq = x ) by A60, NORMSP_1:def 7; :: thesis: verum

ex rseqi being Real_Sequence st

for k being Nat holds

( rseqi . k = (xseq . k) . i & rseqi is convergent & xs . i = lim rseqi ) ) ; :: thesis: verum