:: Double Sequences and Limits
:: by Noboru Endou , Hiroyuki Okazaki and Yasunari Shidama
::
:: Received August 31, 2013
:: Copyright (c) 2013-2021 Association of Mizar Users


:: Convergence in the Pringsheim sense
definition
let Rseq be Function of [:NAT,NAT:],REAL;
attr Rseq is P-convergent means :: DBLSEQ_1:def 1
 ex p being Real st
for e being Real st 0 < e holds
ex N being Nat st
for n, m being Nat st n >= N & m >= N holds
|.((Rseq . (n,m)) - p).| < e;
end;

:: deftheorem defines P-convergent DBLSEQ_1:def 1 :
for Rseq being Function of [:NAT,NAT:],REAL holds
( Rseq is P-convergent iff ex p being Real st
for e being Real st 0 < e holds
ex N being Nat st
for n, m being Nat st n >= N & m >= N holds
|.((Rseq . (n,m)) - p).| < e );

definition
let Rseq be Function of [:NAT,NAT:],REAL;
assume A1: Rseq is P-convergent ;
func P-lim Rseq -> Real means :def6: :: DBLSEQ_1:def 2
 for e being Real st 0 < e holds
ex N being Nat st
for n, m being Nat st n >= N & m >= N holds
|.((Rseq . (n,m)) - it).| < e;
existence
ex b1 being Real st
for e being Real st 0 < e holds
ex N being Nat st
for n, m being Nat st n >= N & m >= N holds
|.((Rseq . (n,m)) - b1).| < e by A1;
uniqueness
for b1, b2 being Real st ( for e being Real st 0 < e holds
ex N being Nat st
for n, m being Nat st n >= N & m >= N holds
|.((Rseq . (n,m)) - b1).| < e ) & ( for e being Real st 0 < e holds
ex N being Nat st
for n, m being Nat st n >= N & m >= N holds
|.((Rseq . (n,m)) - b2).| < e ) holds
b1 = b2
proof end;
end;

:: deftheorem def6 defines P-lim DBLSEQ_1:def 2 :
for Rseq being Function of [:NAT,NAT:],REAL st Rseq is P-convergent holds
for b2 being Real holds
( b2 = P-lim Rseq iff for e being Real st 0 < e holds
ex N being Nat st
for n, m being Nat st n >= N & m >= N holds
|.((Rseq . (n,m)) - b2).| < e );

definition
let Rseq be Function of [:NAT,NAT:],REAL;
attr Rseq is convergent_in_cod1 means :: DBLSEQ_1:def 3
 for m being Element of NAT holds ProjMap2 (Rseq,m) is convergent ;
attr Rseq is convergent_in_cod2 means :: DBLSEQ_1:def 4
 for n being Element of NAT holds ProjMap1 (Rseq,n) is convergent ;
end;

:: deftheorem defines convergent_in_cod1 DBLSEQ_1:def 3 :
for Rseq being Function of [:NAT,NAT:],REAL holds
( Rseq is convergent_in_cod1 iff for m being Element of NAT holds ProjMap2 (Rseq,m) is convergent );

:: deftheorem defines convergent_in_cod2 DBLSEQ_1:def 4 :
for Rseq being Function of [:NAT,NAT:],REAL holds
( Rseq is convergent_in_cod2 iff for n being Element of NAT holds ProjMap1 (Rseq,n) is convergent );

definition
let Rseq be Function of [:NAT,NAT:],REAL;
func lim_in_cod1 Rseq -> Function of NAT,REAL means :def32: :: DBLSEQ_1:def 5
 for m being Element of NAT holds it . m = lim (ProjMap2 (Rseq,m));
existence
ex b1 being Function of NAT,REAL st
for m being Element of NAT holds b1 . m = lim (ProjMap2 (Rseq,m))
proof end;
uniqueness
for b1, b2 being Function of NAT,REAL st ( for m being Element of NAT holds b1 . m = lim (ProjMap2 (Rseq,m)) ) & ( for m being Element of NAT holds b2 . m = lim (ProjMap2 (Rseq,m)) ) holds
b1 = b2
proof end;
end;

:: deftheorem def32 defines lim_in_cod1 DBLSEQ_1:def 5 :
for Rseq being Function of [:NAT,NAT:],REAL
for b2 being Function of NAT,REAL holds
( b2 = lim_in_cod1 Rseq iff for m being Element of NAT holds b2 . m = lim (ProjMap2 (Rseq,m)) );

definition
let Rseq be Function of [:NAT,NAT:],REAL;
func lim_in_cod2 Rseq -> Function of NAT,REAL means :def33: :: DBLSEQ_1:def 6
 for n being Element of NAT holds it . n = lim (ProjMap1 (Rseq,n));
existence
ex b1 being Function of NAT,REAL st
for n being Element of NAT holds b1 . n = lim (ProjMap1 (Rseq,n))
proof end;
uniqueness
for b1, b2 being Function of NAT,REAL st ( for n being Element of NAT holds b1 . n = lim (ProjMap1 (Rseq,n)) ) & ( for n being Element of NAT holds b2 . n = lim (ProjMap1 (Rseq,n)) ) holds
b1 = b2
proof end;
end;

:: deftheorem def33 defines lim_in_cod2 DBLSEQ_1:def 6 :
for Rseq being Function of [:NAT,NAT:],REAL
for b2 being Function of NAT,REAL holds
( b2 = lim_in_cod2 Rseq iff for n being Element of NAT holds b2 . n = lim (ProjMap1 (Rseq,n)) );

definition
let Rseq be Function of [:NAT,NAT:],REAL;
assume a2: lim_in_cod1 Rseq is convergent ;
func cod1_major_iterated_lim Rseq -> Real means :def34: :: DBLSEQ_1:def 7
 for e being Real st 0 < e holds
ex M being Nat st
for m being Nat st m >= M holds
|.(((lim_in_cod1 Rseq) . m) - it).| < e;
existence
ex b1 being Real st
for e being Real st 0 < e holds
ex M being Nat st
for m being Nat st m >= M holds
|.(((lim_in_cod1 Rseq) . m) - b1).| < e by a2, SEQ_2:def 6;
uniqueness
for b1, b2 being Real st ( for e being Real st 0 < e holds
ex M being Nat st
for m being Nat st m >= M holds
|.(((lim_in_cod1 Rseq) . m) - b1).| < e ) & ( for e being Real st 0 < e holds
ex M being Nat st
for m being Nat st m >= M holds
|.(((lim_in_cod1 Rseq) . m) - b2).| < e ) holds
b1 = b2
proof end;
end;

:: deftheorem def34 defines cod1_major_iterated_lim DBLSEQ_1:def 7 :
for Rseq being Function of [:NAT,NAT:],REAL st lim_in_cod1 Rseq is convergent holds
for b2 being Real holds
( b2 = cod1_major_iterated_lim Rseq iff for e being Real st 0 < e holds
ex M being Nat st
for m being Nat st m >= M holds
|.(((lim_in_cod1 Rseq) . m) - b2).| < e );

definition
let Rseq be Function of [:NAT,NAT:],REAL;
assume a2: lim_in_cod2 Rseq is convergent ;
func cod2_major_iterated_lim Rseq -> Real means :def35: :: DBLSEQ_1:def 8
 for e being Real st 0 < e holds
ex N being Nat st
for n being Nat st n >= N holds
|.(((lim_in_cod2 Rseq) . n) - it).| < e;
existence
ex b1 being Real st
for e being Real st 0 < e holds
ex N being Nat st
for n being Nat st n >= N holds
|.(((lim_in_cod2 Rseq) . n) - b1).| < e by a2, SEQ_2:def 6;
uniqueness
for b1, b2 being Real st ( for e being Real st 0 < e holds
ex N being Nat st
for n being Nat st n >= N holds
|.(((lim_in_cod2 Rseq) . n) - b1).| < e ) & ( for e being Real st 0 < e holds
ex N being Nat st
for n being Nat st n >= N holds
|.(((lim_in_cod2 Rseq) . n) - b2).| < e ) holds
b1 = b2
proof end;
end;

:: deftheorem def35 defines cod2_major_iterated_lim DBLSEQ_1:def 8 :
for Rseq being Function of [:NAT,NAT:],REAL st lim_in_cod2 Rseq is convergent holds
for b2 being Real holds
( b2 = cod2_major_iterated_lim Rseq iff for e being Real st 0 < e holds
ex N being Nat st
for n being Nat st n >= N holds
|.(((lim_in_cod2 Rseq) . n) - b2).| < e );

definition
let Rseq be Function of [:NAT,NAT:],REAL;
attr Rseq is uniformly_convergent_in_cod1 means :: DBLSEQ_1:def 9
( Rseq is convergent_in_cod1 & ( for e being Real st e > 0 holds
ex M being Nat st
for m being Nat st m >= M holds
for n being Nat holds |.((Rseq . (n,m)) - ((lim_in_cod1 Rseq) . n)).| < e ) );
end;

:: deftheorem defines uniformly_convergent_in_cod1 DBLSEQ_1:def 9 :
for Rseq being Function of [:NAT,NAT:],REAL holds
( Rseq is uniformly_convergent_in_cod1 iff ( Rseq is convergent_in_cod1 & ( for e being Real st e > 0 holds
ex M being Nat st
for m being Nat st m >= M holds
for n being Nat holds |.((Rseq . (n,m)) - ((lim_in_cod1 Rseq) . n)).| < e ) ) );

definition
let Rseq be Function of [:NAT,NAT:],REAL;
attr Rseq is uniformly_convergent_in_cod2 means :: DBLSEQ_1:def 10
( Rseq is convergent_in_cod2 & ( for e being Real st e > 0 holds
ex N being Nat st
for n being Nat st n >= N holds
for m being Nat holds |.((Rseq . (n,m)) - ((lim_in_cod2 Rseq) . m)).| < e ) );
end;

:: deftheorem defines uniformly_convergent_in_cod2 DBLSEQ_1:def 10 :
for Rseq being Function of [:NAT,NAT:],REAL holds
( Rseq is uniformly_convergent_in_cod2 iff ( Rseq is convergent_in_cod2 & ( for e being Real st e > 0 holds
ex N being Nat st
for n being Nat st n >= N holds
for m being Nat holds |.((Rseq . (n,m)) - ((lim_in_cod2 Rseq) . m)).| < e ) ) );

definition
let Rseq be Function of [:NAT,NAT:],REAL;
attr Rseq is non-decreasing means :: DBLSEQ_1:def 11
 for n1, m1, n2, m2 being Nat st n1 >= n2 & m1 >= m2 holds
Rseq . (n1,m1) >= Rseq . (n2,m2);
attr Rseq is non-increasing means :: DBLSEQ_1:def 12
 for n1, m1, n2, m2 being Nat st n1 >= n2 & m1 >= m2 holds
Rseq . (n1,m1) <= Rseq . (n2,m2);
end;

:: deftheorem defines non-decreasing DBLSEQ_1:def 11 :
for Rseq being Function of [:NAT,NAT:],REAL holds
( Rseq is non-decreasing iff for n1, m1, n2, m2 being Nat st n1 >= n2 & m1 >= m2 holds
Rseq . (n1,m1) >= Rseq . (n2,m2) );

:: deftheorem defines non-increasing DBLSEQ_1:def 12 :
for Rseq being Function of [:NAT,NAT:],REAL holds
( Rseq is non-increasing iff for n1, m1, n2, m2 being Nat st n1 >= n2 & m1 >= m2 holds
Rseq . (n1,m1) <= Rseq . (n2,m2) );

theorem th28: :: DBLSEQ_1:1
for a, b, c being Real st a <= b & b <= c & not |.b.| <= |.a.| holds
|.b.| <= |.c.|
proof end;

registration
cluster Function-like V32([:NAT,NAT:], REAL ) P-convergent non-decreasing -> bounded_above bounded_below for Element of bool [:[:NAT,NAT:],REAL:];
coherence
for b1 being Function of [:NAT,NAT:],REAL st b1 is non-decreasing & b1 is P-convergent holds
( b1 is bounded_below & b1 is bounded_above )
proof end;
end;

registration
cluster Function-like V32([:NAT,NAT:], REAL ) P-convergent non-increasing -> bounded_above bounded_below for Element of bool [:[:NAT,NAT:],REAL:];
coherence
for b1 being Function of [:NAT,NAT:],REAL st b1 is non-increasing & b1 is P-convergent holds
( b1 is bounded_below & b1 is bounded_above )
proof end;
end;

LM111: for r being Element of REAL holds
( [:NAT,NAT:] --> r is P-convergent & [:NAT,NAT:] --> r is convergent_in_cod1 & [:NAT,NAT:] --> r is convergent_in_cod2 )
proof end;

registration
let r be Element of REAL ;
cluster [:NAT,NAT:] --> r -> P-convergent convergent_in_cod1 convergent_in_cod2 for Function of [:NAT,NAT:],REAL;
coherence
for b1 being Function of [:NAT,NAT:],REAL st b1 = [:NAT,NAT:] --> r holds
( b1 is P-convergent & b1 is convergent_in_cod1 & b1 is convergent_in_cod2 ) by LM111;
end;

theorem :: DBLSEQ_1:2
for r being Element of REAL holds P-lim ([:NAT,NAT:] --> r) = r
proof end;

registration
cluster non empty Relation-like [:NAT,NAT:] -defined REAL -valued Function-like V28([:NAT,NAT:]) V32([:NAT,NAT:], REAL ) V109() V110() V111() P-convergent convergent_in_cod1 convergent_in_cod2 for Element of bool [:[:NAT,NAT:],REAL:];
existence
ex b1 being Function of [:NAT,NAT:],REAL st
( b1 is P-convergent & b1 is convergent_in_cod1 & b1 is convergent_in_cod2 )
proof end;
end;

registration
let Pseq2 be P-convergent convergent_in_cod2 Function of [:NAT,NAT:],REAL;
cluster lim_in_cod2 Pseq2 -> convergent ;
coherence
lim_in_cod2 Pseq2 is convergent
proof end;
end;

theorem :: DBLSEQ_1:3
for Rseq being Function of [:NAT,NAT:],REAL st Rseq is P-convergent & Rseq is convergent_in_cod2 holds
P-lim Rseq = cod2_major_iterated_lim Rseq
proof end;

registration
let Pseq1 be P-convergent convergent_in_cod1 Function of [:NAT,NAT:],REAL;
cluster lim_in_cod1 Pseq1 -> convergent ;
coherence
lim_in_cod1 Pseq1 is convergent
proof end;
end;

theorem :: DBLSEQ_1:4
for Rseq being Function of [:NAT,NAT:],REAL st Rseq is P-convergent & Rseq is convergent_in_cod1 holds
P-lim Rseq = cod1_major_iterated_lim Rseq
proof end;

LM112: for Rseq being Function of [:NAT,NAT:],REAL st Rseq is non-decreasing & Rseq is bounded_above holds
( Rseq is P-convergent & Rseq is convergent_in_cod1 & Rseq is convergent_in_cod2 )
proof end;

registration
cluster Function-like V32([:NAT,NAT:], REAL ) bounded_above non-decreasing -> P-convergent convergent_in_cod1 convergent_in_cod2 for Element of bool [:[:NAT,NAT:],REAL:];
coherence
for b1 being Function of [:NAT,NAT:],REAL st b1 is non-decreasing & b1 is bounded_above holds
( b1 is P-convergent & b1 is convergent_in_cod1 & b1 is convergent_in_cod2 ) by LM112;
end;

LM113: for Rseq being Function of [:NAT,NAT:],REAL st Rseq is non-increasing & Rseq is bounded_below holds
( Rseq is P-convergent & Rseq is convergent_in_cod1 & Rseq is convergent_in_cod2 )
proof end;

registration
cluster Function-like V32([:NAT,NAT:], REAL ) bounded_below non-increasing -> P-convergent convergent_in_cod1 convergent_in_cod2 for Element of bool [:[:NAT,NAT:],REAL:];
coherence
for b1 being Function of [:NAT,NAT:],REAL st b1 is non-increasing & b1 is bounded_below holds
( b1 is P-convergent & b1 is convergent_in_cod1 & b1 is convergent_in_cod2 ) by LM113;
end;

theorem :: DBLSEQ_1:5
for Rseq being Function of [:NAT,NAT:],REAL st Rseq is uniformly_convergent_in_cod1 & lim_in_cod1 Rseq is convergent holds
( Rseq is P-convergent & P-lim Rseq = cod1_major_iterated_lim Rseq )
proof end;

theorem :: DBLSEQ_1:6
for Rseq being Function of [:NAT,NAT:],REAL st Rseq is uniformly_convergent_in_cod2 & lim_in_cod2 Rseq is convergent holds
( Rseq is P-convergent & P-lim Rseq = cod2_major_iterated_lim Rseq )
proof end;

definition
let Rseq be Function of [:NAT,NAT:],REAL;
attr Rseq is Cauchy means :: DBLSEQ_1:def 13
 for e being Real st e > 0 holds
ex N being Nat st
for n1, n2, m1, m2 being Nat st N <= n1 & n1 <= n2 & N <= m1 & m1 <= m2 holds
|.((Rseq . (n2,m2)) - (Rseq . (n1,m1))).| < e;
end;

:: deftheorem defines Cauchy DBLSEQ_1:def 13 :
for Rseq being Function of [:NAT,NAT:],REAL holds
( Rseq is Cauchy iff for e being Real st e > 0 holds
ex N being Nat st
for n1, n2, m1, m2 being Nat st N <= n1 & n1 <= n2 & N <= m1 & m1 <= m2 holds
|.((Rseq . (n2,m2)) - (Rseq . (n1,m1))).| < e );

theorem :: DBLSEQ_1:7
for Rseq being Function of [:NAT,NAT:],REAL holds
( Rseq is P-convergent iff Rseq is Cauchy )
proof end;

theorem :: DBLSEQ_1:8
for Rseq being Function of [:NAT,NAT:],REAL st ( Rseq is non-decreasing or Rseq is non-increasing ) holds
( Rseq is P-convergent iff ( Rseq is bounded_below & Rseq is bounded_above ) ) ;

definition
let X, Y be non empty set ;
let H be BinOp of Y;
let f, g be Function of X,Y;
:: original: *
redefine func H * (f,g) -> Function of [:X,X:],Y;
coherence
H * (f,g) is Function of [:X,X:],Y
proof end;
end;

theorem :: DBLSEQ_1:9
for rseq1, rseq2 being convergent Real_Sequence holds
( multreal * (rseq1,rseq2) is convergent_in_cod1 & multreal * (rseq1,rseq2) is convergent_in_cod2 & lim_in_cod1 (multreal * (rseq1,rseq2)) is convergent & cod1_major_iterated_lim (multreal * (rseq1,rseq2)) = (lim rseq1) * (lim rseq2) & lim_in_cod2 (multreal * (rseq1,rseq2)) is convergent & cod2_major_iterated_lim (multreal * (rseq1,rseq2)) = (lim rseq1) * (lim rseq2) & multreal * (rseq1,rseq2) is P-convergent & P-lim (multreal * (rseq1,rseq2)) = (lim rseq1) * (lim rseq2) )
proof end;

theorem :: DBLSEQ_1:10
for rseq1, rseq2 being convergent Real_Sequence holds
( addreal * (rseq1,rseq2) is convergent_in_cod1 & addreal * (rseq1,rseq2) is convergent_in_cod2 & lim_in_cod1 (addreal * (rseq1,rseq2)) is convergent & cod1_major_iterated_lim (addreal * (rseq1,rseq2)) = (lim rseq1) + (lim rseq2) & lim_in_cod2 (addreal * (rseq1,rseq2)) is convergent & cod2_major_iterated_lim (addreal * (rseq1,rseq2)) = (lim rseq1) + (lim rseq2) & addreal * (rseq1,rseq2) is P-convergent & P-lim (addreal * (rseq1,rseq2)) = (lim rseq1) + (lim rseq2) )
proof end;

lmADD: for Rseq1, Rseq2 being Function of [:NAT,NAT:],REAL holds
( dom (Rseq1 + Rseq2) = [:NAT,NAT:] & dom (Rseq1 - Rseq2) = [:NAT,NAT:] & ( for n, m being Nat holds (Rseq1 + Rseq2) . (n,m) = (Rseq1 . (n,m)) + (Rseq2 . (n,m)) ) & ( for n, m being Nat holds (Rseq1 - Rseq2) . (n,m) = (Rseq1 . (n,m)) - (Rseq2 . (n,m)) ) )
proof end;

theorem :: DBLSEQ_1:11
for Rseq1, Rseq2 being Function of [:NAT,NAT:],REAL st Rseq1 is P-convergent & Rseq2 is P-convergent holds
( Rseq1 + Rseq2 is P-convergent & P-lim (Rseq1 + Rseq2) = (P-lim Rseq1) + (P-lim Rseq2) )
proof end;

theorem th54b: :: DBLSEQ_1:12
for Rseq1, Rseq2 being Function of [:NAT,NAT:],REAL st Rseq1 is P-convergent & Rseq2 is P-convergent holds
( Rseq1 - Rseq2 is P-convergent & P-lim (Rseq1 - Rseq2) = (P-lim Rseq1) - (P-lim Rseq2) )
proof end;

lm55a: for Rseq being Function of [:NAT,NAT:],REAL
for a being Real st ( for n, m being Nat holds Rseq . (n,m) = a ) holds
( Rseq is P-convergent & P-lim Rseq = a )
proof end;

theorem :: DBLSEQ_1:13
for Rseq being Function of [:NAT,NAT:],REAL
for r being Real st Rseq is P-convergent holds
( r (#) Rseq is P-convergent & P-lim (r (#) Rseq) = r * (P-lim Rseq) )
proof end;

theorem th55b: :: DBLSEQ_1:14
for Rseq being Function of [:NAT,NAT:],REAL
for r being Real st Rseq is P-convergent & ( for n, m being Nat holds Rseq . (n,m) >= r ) holds
P-lim Rseq >= r
proof end;

theorem :: DBLSEQ_1:15
for Rseq1, Rseq2 being Function of [:NAT,NAT:],REAL st Rseq1 is P-convergent & Rseq2 is P-convergent & ( for n, m being Nat holds Rseq1 . (n,m) <= Rseq2 . (n,m) ) holds
P-lim Rseq1 <= P-lim Rseq2
proof end;

theorem :: DBLSEQ_1:16
for Rseq, Rseq1, Rseq2 being Function of [:NAT,NAT:],REAL st Rseq1 is P-convergent & Rseq2 is P-convergent & P-lim Rseq1 = P-lim Rseq2 & ( for n, m being Nat holds
( Rseq1 . (n,m) <= Rseq . (n,m) & Rseq . (n,m) <= Rseq2 . (n,m) ) ) holds
( Rseq is P-convergent & P-lim Rseq = P-lim Rseq1 )
proof end;

definition
let X be non empty set ;
let seq be Function of [:NAT,NAT:],X;
mode subsequence of seq -> Function of [:NAT,NAT:],X means :def9: :: DBLSEQ_1:def 14
 ex N, M being V113() sequence of NAT st
for n, m being Nat holds it . (n,m) = seq . ((N . n),(M . m));
existence
ex b1 being Function of [:NAT,NAT:],X ex N, M being V113() sequence of NAT st
for n, m being Nat holds b1 . (n,m) = seq . ((N . n),(M . m))
proof end;
end;

:: deftheorem def9 defines subsequence DBLSEQ_1:def 14 :
for X being non empty set
for seq, b3 being Function of [:NAT,NAT:],X holds
( b3 is subsequence of seq iff ex N, M being V113() sequence of NAT st
for n, m being Nat holds b3 . (n,m) = seq . ((N . n),(M . m)) );

lem01: for seq being V113() sequence of NAT
for n being Nat holds n <= seq . n
proof end;

LM114: for Rseq being Function of [:NAT,NAT:],REAL
for Rseq1 being subsequence of Rseq st Rseq is P-convergent holds
( Rseq1 is P-convergent & P-lim Rseq1 = P-lim Rseq )
proof end;

th63d: for Rseq being Function of [:NAT,NAT:],REAL st Rseq is convergent_in_cod1 holds
for Rseq1 being subsequence of Rseq holds Rseq1 is convergent_in_cod1
proof end;

registration
let Pseq be P-convergent Function of [:NAT,NAT:],REAL;
cluster -> P-convergent for subsequence of Pseq;
coherence
for b1 being subsequence of Pseq holds b1 is P-convergent by LM114;
end;

theorem :: DBLSEQ_1:17
for Pseq being P-convergent Function of [:NAT,NAT:],REAL
for Psubseq being subsequence of Pseq holds P-lim Psubseq = P-lim Pseq by LM114;

registration
let Rseq be convergent_in_cod1 Function of [:NAT,NAT:],REAL;
cluster -> convergent_in_cod1 for subsequence of Rseq;
coherence
for b1 being subsequence of Rseq holds b1 is convergent_in_cod1 by th63d;
end;

theorem :: DBLSEQ_1:18
for Rseq being Function of [:NAT,NAT:],REAL
for Rseq1 being subsequence of Rseq st Rseq is convergent_in_cod1 & lim_in_cod1 Rseq is convergent holds
( lim_in_cod1 Rseq1 is convergent & cod1_major_iterated_lim Rseq1 = cod1_major_iterated_lim Rseq )
proof end;

th63c: for Rseq being Function of [:NAT,NAT:],REAL st Rseq is convergent_in_cod2 holds
for Rseq1 being subsequence of Rseq holds Rseq1 is convergent_in_cod2
proof end;

registration
let Rseq be convergent_in_cod2 Function of [:NAT,NAT:],REAL;
cluster -> convergent_in_cod2 for subsequence of Rseq;
coherence
for b1 being subsequence of Rseq holds b1 is convergent_in_cod2 by th63c;
end;

theorem :: DBLSEQ_1:19
for Rseq being Function of [:NAT,NAT:],REAL
for Rseq1 being subsequence of Rseq st Rseq is convergent_in_cod2 & lim_in_cod2 Rseq is convergent holds
( lim_in_cod2 Rseq1 is convergent & cod2_major_iterated_lim Rseq1 = cod2_major_iterated_lim Rseq )
proof end;