let Rseq be Function of [:NAT,NAT:],REAL; :: thesis: 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 )
let Rseq1 be subsequence of Rseq; :: thesis: ( Rseq is convergent_in_cod2 & lim_in_cod2 Rseq is convergent implies ( lim_in_cod2 Rseq1 is convergent & cod2_major_iterated_lim Rseq1 = cod2_major_iterated_lim Rseq ) )
assume a1: ( Rseq is convergent_in_cod2 & lim_in_cod2 Rseq is convergent ) ; :: thesis: ( lim_in_cod2 Rseq1 is convergent & cod2_major_iterated_lim Rseq1 = cod2_major_iterated_lim Rseq )
consider I1, I2 being increasing sequence of NAT such that
a7: for n, m being Nat holds Rseq1 . (n,m) = Rseq . ((I1 . n),(I2 . m)) by def9;
a8: Rseq1 is convergent_in_cod2 by a1;
a10: for e being Real st 0 < e holds
ex N being Nat st
for m being Nat st m >= N holds
|.(((lim_in_cod2 Rseq1) . m) - (cod2_major_iterated_lim Rseq)).| < e

proof

let e be Real; :: thesis: ( 0 < e implies ex N being Nat st
for m being Nat st m >= N holds
|.(((lim_in_cod2 Rseq1) . m) - (cod2_major_iterated_lim Rseq)).| < e )
assume 0 < e ; :: thesis: ex N being Nat st
for m being Nat st m >= N holds
|.(((lim_in_cod2 Rseq1) . m) - (cod2_major_iterated_lim Rseq)).| < e
then consider N being Nat such that
a11: for m being Nat st m >= N holds
|.(((lim_in_cod2 Rseq) . m) - (cod2_major_iterated_lim Rseq)).| < e by a1, def35;
take N ; :: thesis: for m being Nat st m >= N holds
|.(((lim_in_cod2 Rseq1) . m) - (cod2_major_iterated_lim Rseq)).| < e

hereby :: thesis: verum

let m be Nat; :: thesis: ( m >= N implies |.(((lim_in_cod2 Rseq1) . m) - (cod2_major_iterated_lim Rseq)).| < e )
reconsider mm = m as Element of NAT by ORDINAL1:def 12;
assume a12: m >= N ; :: thesis: |.(((lim_in_cod2 Rseq1) . m) - (cod2_major_iterated_lim Rseq)).| < e
reconsider m1 = I1 . m as Element of NAT ;
x2: ProjMap1 (Rseq1,mm) is convergent by a8;
for p being Real st 0 < p holds
ex K being Nat st
for n being Nat st n >= K holds
|.(((ProjMap1 (Rseq1,mm)) . n) - (lim (ProjMap1 (Rseq,m1)))).| < p

proof

let p be Real; :: thesis: ( 0 < p implies ex K being Nat st
for n being Nat st n >= K holds
|.(((ProjMap1 (Rseq1,mm)) . n) - (lim (ProjMap1 (Rseq,m1)))).| < p )
assume b1: 0 < p ; :: thesis: ex K being Nat st
for n being Nat st n >= K holds
|.(((ProjMap1 (Rseq1,mm)) . n) - (lim (ProjMap1 (Rseq,m1)))).| < p
ProjMap1 (Rseq,m1) is convergent by a1;
then consider K being Nat such that
b2: for n being Nat st n >= K holds
|.(((ProjMap1 (Rseq,m1)) . n) - (lim (ProjMap1 (Rseq,m1)))).| < p by b1, SEQ_2:def 7;
take K ; :: thesis: for n being Nat st n >= K holds
|.(((ProjMap1 (Rseq1,mm)) . n) - (lim (ProjMap1 (Rseq,m1)))).| < p

hereby :: thesis: verum

let n be Nat; :: thesis: ( n >= K implies |.(((ProjMap1 (Rseq1,mm)) . n) - (lim (ProjMap1 (Rseq,m1)))).| < p )
assume b3: n >= K ; :: thesis: |.(((ProjMap1 (Rseq1,mm)) . n) - (lim (ProjMap1 (Rseq,m1)))).| < p
x3: ( n is Element of NAT & I1 . m is Element of NAT & I2 . n is Element of NAT ) by ORDINAL1:def 12;
I2 . n >= n by lem01;
then I2 . n >= K by b3, XXREAL_0:2;
then |.(((ProjMap1 (Rseq,m1)) . (I2 . n)) - (lim (ProjMap1 (Rseq,m1)))).| < p by b2;
then |.((Rseq . ((I1 . m),(I2 . n))) - (lim (ProjMap1 (Rseq,m1)))).| < p by MESFUNC9:def 6;
then |.((Rseq1 . (m,n)) - (lim (ProjMap1 (Rseq,m1)))).| < p by a7;
hence |.(((ProjMap1 (Rseq1,mm)) . n) - (lim (ProjMap1 (Rseq,m1)))).| < p by x3, MESFUNC9:def 6; :: thesis: verum

end;

end;

then c1: lim (ProjMap1 (Rseq1,mm)) = lim (ProjMap1 (Rseq,m1)) by x2, SEQ_2:def 7;
I1 . m >= m by lem01;
then I1 . m >= N by a12, XXREAL_0:2;
then a13: |.(((lim_in_cod2 Rseq) . (I1 . m)) - (cod2_major_iterated_lim Rseq)).| < e by a11;
(lim_in_cod2 Rseq) . (I1 . m) = lim (ProjMap1 (Rseq,m1)) by def33;
hence |.(((lim_in_cod2 Rseq1) . m) - (cod2_major_iterated_lim Rseq)).| < e by def33, a13, c1; :: thesis: verum

end;

end;

hence lim_in_cod2 Rseq1 is convergent by SEQ_2:def 6; :: thesis: cod2_major_iterated_lim Rseq1 = cod2_major_iterated_lim Rseq
hence cod2_major_iterated_lim Rseq1 = cod2_major_iterated_lim Rseq by a10, def35; :: thesis: verum