let Rseq be Function of [:NAT,NAT:],REAL; :: thesis: 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 )
let Rseq1 be subsequence of Rseq; :: thesis: ( Rseq is convergent_in_cod1 & lim_in_cod1 Rseq is convergent implies ( lim_in_cod1 Rseq1 is convergent & cod1_major_iterated_lim Rseq1 = cod1_major_iterated_lim Rseq ) )
assume a1: ( Rseq is convergent_in_cod1 & lim_in_cod1 Rseq is convergent ) ; :: thesis: ( lim_in_cod1 Rseq1 is convergent & cod1_major_iterated_lim Rseq1 = cod1_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_cod1 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_cod1 Rseq1) . m) - (cod1_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_cod1 Rseq1) . m) - (cod1_major_iterated_lim Rseq)).| < e )
assume 0 < e ; :: thesis: ex N being Nat st
for m being Nat st m >= N holds
|.(((lim_in_cod1 Rseq1) . m) - (cod1_major_iterated_lim Rseq)).| < e
then consider N being Nat such that
a11: for m being Nat st m >= N holds
|.(((lim_in_cod1 Rseq) . m) - (cod1_major_iterated_lim Rseq)).| < e by a1, def34;
take N ; :: thesis: for m being Nat st m >= N holds
|.(((lim_in_cod1 Rseq1) . m) - (cod1_major_iterated_lim Rseq)).| < e

hereby :: thesis: verum

let m be Nat; :: thesis: ( m >= N implies |.(((lim_in_cod1 Rseq1) . m) - (cod1_major_iterated_lim Rseq)).| < e )
assume a12: m >= N ; :: thesis: |.(((lim_in_cod1 Rseq1) . m) - (cod1_major_iterated_lim Rseq)).| < e
reconsider m2 = I2 . m as Element of NAT ;
reconsider m1 = m as Element of NAT by ORDINAL1:def 12;
x2: ProjMap2 (Rseq1,m1) 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
|.(((ProjMap2 (Rseq1,m1)) . n) - (lim (ProjMap2 (Rseq,m2)))).| < p

proof

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

hereby :: thesis: verum

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

end;

end;

then c1: lim (ProjMap2 (Rseq1,m1)) = lim (ProjMap2 (Rseq,m2)) by x2, SEQ_2:def 7;
I2 . m >= m by lem01;
then I2 . m >= N by a12, XXREAL_0:2;
then a13: |.(((lim_in_cod1 Rseq) . (I2 . m)) - (cod1_major_iterated_lim Rseq)).| < e by a11;
(lim_in_cod1 Rseq) . (I2 . m) = lim (ProjMap2 (Rseq,m2)) by def32;
hence |.(((lim_in_cod1 Rseq1) . m) - (cod1_major_iterated_lim Rseq)).| < e by def32, a13, c1; :: thesis: verum

end;

end;

hence lim_in_cod1 Rseq1 is convergent by SEQ_2:def 6; :: thesis: cod1_major_iterated_lim Rseq1 = cod1_major_iterated_lim Rseq
hence cod1_major_iterated_lim Rseq1 = cod1_major_iterated_lim Rseq by a10, def34; :: thesis: verum