defpred S₁[ Nat] means for x being sequence of (REAL-NS $1) st ex K being Real st
for i being Nat holds ||.(x . i).|| < K holds
ex x0 being subsequence of x st x0 is convergent ;
A1: S₁[ 0 ]

proof

let x be sequence of (REAL-NS 0); :: thesis: ( ex K being Real st
for i being Nat holds ||.(x . i).|| < K implies ex x0 being subsequence of x st x0 is convergent )
assume ex K being Real st
for i being Nat holds ||.(x . i).|| < K ; :: thesis: ex x0 being subsequence of x st x0 is convergent
A2: the carrier of (REAL-NS 0) = REAL 0 by REAL_NS1:def 4
.= {(<*> REAL)} by FINSEQ_2:94 ;
then reconsider z = <*> REAL as Element of (REAL-NS 0) by TARSKI:def 1;
for i being Nat holds x . i = z by A2, TARSKI:def 1;
then A3: x is constant by VALUED_0:def 18;
A4: x is subsequence of x by VALUED_0:19;
x is convergent by A3, NDIFF_1:18;
hence ex x0 being subsequence of x st x0 is convergent by A4; :: thesis: verum

end;

A5: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A6: S₁[n] ; :: thesis: S₁[n + 1]
let x be sequence of (REAL-NS (n + 1)); :: thesis: ( ex K being Real st
for i being Nat holds ||.(x . i).|| < K implies ex x0 being subsequence of x st x0 is convergent )
given K being Real such that A7: for i being Nat holds ||.(x . i).|| < K ; :: thesis: ex x0 being subsequence of x st x0 is convergent
defpred S₂[ object , object ] means ex xi being Element of REAL (n + 1) st
( xi = x . $1 & $2 = xi | n );
A8: for i being Element of NAT ex y being Element of the carrier of (REAL-NS n) st S₂[i,y]

proof

let i be Element of NAT ; :: thesis: ex y being Element of the carrier of (REAL-NS n) st S₂[i,y]
reconsider xi = x . i as Element of REAL (n + 1) by REAL_NS1:def 4;
A9: len xi = n + 1 by CARD_1:def 7;
set y = xi | n;
A10: xi | n is Element of (len (xi | n)) -tuples_on REAL by FINSEQ_2:92;
len (xi | n) = n by A9, NAT_1:11, FINSEQ_1:59;
then xi | n in REAL n by A10;
then reconsider y = xi | n as Element of the carrier of (REAL-NS n) by REAL_NS1:def 4;
take y ; :: thesis: S₂[i,y]
thus S₂[i,y] ; :: thesis: verum

end;

consider y being sequence of the carrier of (REAL-NS n) such that
A11: for i being Element of NAT holds S₂[i,y . i] from FUNCT_2:sch 3(A8);
reconsider y = y as sequence of (REAL-NS n) ;
for i being Nat holds ||.(y . i).|| < K

proof

let i be Nat; :: thesis: ||.(y . i).|| < K
i is Element of NAT by ORDINAL1:def 12;
then consider xi being Element of REAL (n + 1) such that
A12: ( xi = x . i & y . i = xi | n ) by A11;
reconsider yi = y . i as Element of REAL n by REAL_NS1:def 4;
A13: |.yi.| <= |.xi.| by A12, Th1;
||.(x . i).|| < K by A7;
then |.xi.| < K by A12, REAL_NS1:1;
then |.yi.| < K by A13, XXREAL_0:2;
hence ||.(y . i).|| < K by REAL_NS1:1; :: thesis: verum

end;

then consider y0 being subsequence of y such that
A14: y0 is convergent by A6;
consider N0 being increasing sequence of NAT such that
A15: y0 = y * N0 by VALUED_0:def 17;
defpred S₃[ object , object ] means ex xi being Element of REAL (n + 1) st
( xi = (x * N0) . $1 & $2 = xi . (n + 1) );
A16: for i being Element of NAT ex y being Element of REAL st S₃[i,y]

proof

let i be Element of NAT ; :: thesis: ex y being Element of REAL st S₃[i,y]
reconsider xi = (x * N0) . i as Element of REAL (n + 1) by REAL_NS1:def 4;
set y = xi . (n + 1);
take xi . (n + 1) ; :: thesis: ( xi . (n + 1) is Element of REAL & S₃[i,xi . (n + 1)] )
A17: len xi = n + 1 by CARD_1:def 7;
n + 1 in Seg (n + 1) by FINSEQ_1:4;
then n + 1 in dom xi by A17, FINSEQ_1:def 3;
then xi . (n + 1) in rng xi by FUNCT_1:3;
hence ( xi . (n + 1) is Element of REAL & S₃[i,xi . (n + 1)] ) ; :: thesis: verum

end;

consider w being sequence of REAL such that
A18: for i being Element of NAT holds S₃[i,w . i] from FUNCT_2:sch 3(A16);
for i0 being set st i0 in dom w holds
|.(w . i0).| < K

proof

let i0 be set ; :: thesis: ( i0 in dom w implies |.(w . i0).| < K )
assume i0 in dom w ; :: thesis: |.(w . i0).| < K
then reconsider i = i0 as Element of NAT ;
consider xi being Element of REAL (n + 1) such that
A19: ( xi = (x * N0) . i & w . i = xi . (n + 1) ) by A18;
reconsider wi = w . i as Element of REAL ;
A20: |.wi.| <= |.xi.| by A19, Th2;
dom N0 = NAT by FUNCT_2:def 1;
then (x * N0) . i = x . (N0 . i) by FUNCT_1:13;
then ||.((x * N0) . i).|| < K by A7;
then |.xi.| < K by A19, REAL_NS1:1;
hence |.(w . i0).| < K by XXREAL_0:2, A20; :: thesis: verum

end;

then w is bounded by COMSEQ_2:def 3;
then consider w0 being Real_Sequence such that
A21: ( w0 is subsequence of w & w0 is convergent ) by SEQ_4:40;
consider M0 being increasing sequence of NAT such that
A22: w0 = w * M0 by A21, VALUED_0:def 17;
reconsider N = N0 * M0 as increasing sequence of NAT ;
reconsider x0 = x * N as subsequence of x ;
A23: for i being Nat ex xi being Element of REAL (n + 1) st
( xi = x0 . i & (y0 * M0) . i = xi | n & w0 . i = xi . (n + 1) )

proof

let i be Nat; :: thesis: ex xi being Element of REAL (n + 1) st
( xi = x0 . i & (y0 * M0) . i = xi | n & w0 . i = xi . (n + 1) )
A24: ( dom N0 = NAT & dom M0 = NAT ) by FUNCT_2:def 1;
A25: (y0 * M0) . i = y0 . (M0 . i) by A24, ORDINAL1:def 12, FUNCT_1:13
.= y . (N0 . (M0 . i)) by A15, A24, FUNCT_1:13 ;
consider z being Element of REAL (n + 1) such that
A26: ( z = x . (N0 . (M0 . i)) & y . (N0 . (M0 . i)) = z | n ) by A11;
take z ; :: thesis: ( z = x0 . i & (y0 * M0) . i = z | n & w0 . i = z . (n + 1) )
thus A27: x0 . i = ((x * N0) * M0) . i by RELAT_1:36
.= (x * N0) . (M0 . i) by A24, ORDINAL1:def 12, FUNCT_1:13
.= z by A24, A26, FUNCT_1:13 ; :: thesis: ( (y0 * M0) . i = z | n & w0 . i = z . (n + 1) )
thus (y0 * M0) . i = z | n by A25, A26; :: thesis: w0 . i = z . (n + 1)
consider f being Element of REAL (n + 1) such that
A28: ( f = (x * N0) . (M0 . i) & w . (M0 . i) = f . (n + 1) ) by A18;
x0 . i = ((x * N0) * M0) . i by RELAT_1:36
.= f by A24, A28, ORDINAL1:def 12, FUNCT_1:13 ;
hence w0 . i = z . (n + 1) by A22, A24, A27, A28, ORDINAL1:def 12, FUNCT_1:13; :: thesis: verum

end;

A29: y0 * M0 is convergent by A14, LOPBAN_3:7;
set lmy = lim (y0 * M0);
set lmw = lim w0;
reconsider lmy0 = lim (y0 * M0) as Element of REAL n by REAL_NS1:def 4;
A30: len lmy0 = n by CARD_1:def 7;
then A31: dom lmy0 = Seg n by FINSEQ_1:def 3;
set lmx = lmy0 ^ <*(lim w0)*>;
A32: lmy0 ^ <*(lim w0)*> is FinSequence of REAL by FINSEQ_1:75;
len (lmy0 ^ <*(lim w0)*>) = (len lmy0) + (len <*(lim w0)*>) by FINSEQ_1:22
.= n + 1 by A30, FINSEQ_1:40 ;
then lmy0 ^ <*(lim w0)*> is Element of (n + 1) -tuples_on REAL by A32, FINSEQ_2:92;
then lmy0 ^ <*(lim w0)*> in REAL (n + 1) ;
then reconsider lmx = lmy0 ^ <*(lim w0)*> as Element of (REAL-NS (n + 1)) by REAL_NS1:def 4;
for r being Real st 0 < r holds
ex m being Nat st
for i being Nat st m <= i holds
||.((x0 . i) - lmx).|| < r

proof

let r be Real; :: thesis: ( 0 < r implies ex m being Nat st
for i being Nat st m <= i holds
||.((x0 . i) - lmx).|| < r )
assume 0 < r ; :: thesis: ex m being Nat st
for i being Nat st m <= i holds
||.((x0 . i) - lmx).|| < r
then A33: 0 < r / 2 by XREAL_1:215;
then consider m1 being Nat such that
A34: for i being Nat st m1 <= i holds
||.(((y0 * M0) . i) - (lim (y0 * M0))).|| < r / 2 by A29, NORMSP_1:def 7;
consider m2 being Nat such that
A35: for i being Nat st m2 <= i holds
|.((w0 . i) - (lim w0)).| < r / 2 by SEQ_2:def 7, A21, A33;
set m = m1 + m2;
take m1 + m2 ; :: thesis: for i being Nat st m1 + m2 <= i holds
||.((x0 . i) - lmx).|| < r
thus for i being Nat st m1 + m2 <= i holds
||.((x0 . i) - lmx).|| < r :: thesis: verum

proof

let i be Nat; :: thesis: ( m1 + m2 <= i implies ||.((x0 . i) - lmx).|| < r )
assume A36: m1 + m2 <= i ; :: thesis: ||.((x0 . i) - lmx).|| < r
m1 <= m1 + m2 by NAT_1:11;
then m1 <= i by A36, XXREAL_0:2;
then A37: ||.(((y0 * M0) . i) - (lim (y0 * M0))).|| < r / 2 by A34;
m2 <= m1 + m2 by NAT_1:11;
then m2 <= i by A36, XXREAL_0:2;
then A38: |.((w0 . i) - (lim w0)).| < r / 2 by A35;
reconsider lmx0 = lmx as Element of REAL (n + 1) by REAL_NS1:def 4;
reconsider xi = x0 . i as Element of REAL (n + 1) by REAL_NS1:def 4;
reconsider yi = (y0 * M0) . i as Element of REAL n by REAL_NS1:def 4;
consider z being Element of REAL (n + 1) such that
A39: ( z = x0 . i & (y0 * M0) . i = z | n & w0 . i = z . (n + 1) ) by A23;
lmx0 | n = lmy0 by FINSEQ_1:21, A31;
then A41: (xi - lmx0) | n = yi - lmy0 by A39, Th4, NAT_1:11;
A42: ( len <*(lim w0)*> = 1 & <*(lim w0)*> . 1 = lim w0 ) by FINSEQ_1:40;
A43: (xi - lmx0) . (n + 1) = (xi . (n + 1)) - (lmx0 . (n + 1)) by RVSUM_1:27
.= (w0 . i) - (lim w0) by A30, A39, A42, FINSEQ_1:65 ;
A44: ||.((x0 . i) - lmx).|| = |.(xi - lmx0).| by REAL_NS1:5, REAL_NS1:1;
A45: ||.(((y0 * M0) . i) - (lim (y0 * M0))).|| = |.(yi - lmy0).| by REAL_NS1:5, REAL_NS1:1;
(w0 . i) - (lim w0) is Element of REAL by XREAL_0:def 1;
then A46: |.(xi - lmx0).| <= |.(yi - lmy0).| + |.((w0 . i) - (lim w0)).| by A41, A43, Th3;
|.(yi - lmy0).| + |.((w0 . i) - (lim w0)).| < (r / 2) + (r / 2) by A38, A37, A45, XREAL_1:8;
hence ||.((x0 . i) - lmx).|| < r by XXREAL_0:2, A46, A44; :: thesis: verum

end;

end;

then x0 is convergent by NORMSP_1:def 6;
hence ex x0 being subsequence of x st x0 is convergent ; :: thesis: verum

end;

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