defpred S₁[ 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 ) );

let n be Nat; :: thesis:
assume A2: S₁[n] ; :: thesis:

let x be Point of (REAL-NS (n + 1)); :: thesis:
let xs be Element of REAL (n + 1); :: thesis:
let seq be sequence of (REAL-NS (n + 1)); :: thesis:
let xseq be sequence of (REAL (n + 1)); :: thesis:
assume A3: ( xs = x & xseq = seq ) ; :: thesis:

A4: now :: thesis:

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:
thus ( seq is convergent & lim seq = x ) :: thesis:

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₂[ 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₂[i,y]

proof

let i be Element of NAT ; :: thesis:
take y = (xseq . i) | n; :: thesis:
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₂[i,y] ) by Th6; :: thesis:

end;

consider xseqn being sequence of (REAL n) such that
A8: for i being Element of NAT holds S₂[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₁( Nat) -> object = |.((rseqn1 . $1) - (xs . (n + 1))).|;
consider absrseq being Real_Sequence such that
A9: for i being Nat holds absrseq . i = H₁(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 )

proof

let i be Nat; :: thesis:
assume A11: i in Seg n ; :: thesis:
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:

let k be Nat; :: thesis:
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 16
.= (xseqn . k) . i by A8, A14 ; :: thesis:

end;

xsn . i = (xs | (Seg n)) . i by FINSEQ_1:def 16
.= 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:

end;

then A15: xn = lim seqn by A2;
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:

reconsider rxs = xs as Element of (n + 1) -tuples_on REAL by EUCLID:def 1;
let k be Nat; :: thesis:
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:

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:
assume i in dom (((xseq . k) - xs) | n) ; :: thesis:
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 16
.= ((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 16
.= (((xseq . k) | n) . i) - ((xs | n) . i) by FINSEQ_1:def 16
.= ((xseqn . k) - xsn) . i by A8, A27, A19 ; :: thesis:

end;

dom (((xseq . k) - xs) | n) = Seg n by A24, FINSEQ_1:def 3;
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:

end;

then A32: ||.(seq - x).|| (#) ||.(seq - x).|| = (||.(seqn - xn).|| (#) ||.(seqn - xn).||) + (absrseq (#) absrseq) by SEQ_1:7;

A33: now :: thesis:

let e be Real; :: thesis:
assume e > 0 ; :: thesis:
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:

end;

hence ex m being Nat st
for k being Nat st m <= k holds
|.((absrseq . k) - 0).| < e ; :: thesis:

end;

then A35: absrseq is convergent by SEQ_2:def 6;
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

let e be Real; :: thesis:
assume A41: e > 0 ; :: thesis:
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:

let k be Nat; :: thesis:
assume A43: m <= k ; :: thesis:
||.(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:

end;

hence ex m being Nat st
for k being Nat st k >= m holds
||.((seq . k) - x).|| < e ; :: thesis:

end;

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

end;

now :: thesis:

assume A46: ( seq is convergent & lim seq = x ) ; :: thesis:

now :: thesis:

let i be Nat; :: thesis:
assume A47: i in Seg (n + 1) ; :: thesis:
deffunc H₁( Nat) -> set = (xseq . $1) . i;
consider rseqi being Real_Sequence such that
A48: for l being Nat holds rseqi . l = H₁(l) from SEQ_1:sch 1();

A49: now :: thesis:

let e be Real; :: thesis:
assume A50: e > 0 ; :: thesis:
thus ex k being Nat st
for m being Nat st k <= m holds
|.((rseqi . m) - (xs . i)).| < e :: thesis:

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:
let m be Nat; :: thesis:
assume k <= m ; :: thesis:
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:

end;

then A54: rseqi is convergent by SEQ_2:def 6;
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:

end;

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

end;

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 ) ) by A4; :: thesis:

end;

hence S₁[n + 1] ; :: thesis:

end;

A55: S₁[ 0 ]

proof

let x be Point of (REAL-NS 0); :: thesis:
let xs be Element of REAL 0; :: thesis:
let seq be sequence of (REAL-NS 0); :: thesis:
let xseq be sequence of (REAL 0); :: thesis:
assume that
A56: xs = x and
A57: xseq = seq ; :: thesis:

now :: thesis:

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:
A58: for i being Nat holds seq . i = 0. (REAL-NS 0)

proof

let i be Nat; :: thesis:
xseq . i = 0.REAL 0 ;
hence seq . i = 0. (REAL-NS 0) by A57, Def4; :: thesis:

end;

xs = 0* 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

proof

let r be Real; :: thesis:
assume A61: 0 < r ; :: thesis:
take m = 1; :: thesis:
let k be Nat; :: thesis:
assume m <= k ; :: thesis:
||.((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:

end;

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

end;

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

end;

thus for n being Nat holds S₁[n] from NAT_1:sch 2(A55, A1); :: thesis: