let Rseq be Function of [:NAT,NAT:],REAL; :: thesis: ( Rseq is convergent_in_cod2 implies for Rseq1 being subsequence of Rseq holds Rseq1 is convergent_in_cod2 )
assume a1: Rseq is convergent_in_cod2 ; :: thesis: for Rseq1 being subsequence of Rseq holds Rseq1 is convergent_in_cod2

hereby :: thesis: verum

let Rseq1 be subsequence of Rseq; :: thesis: Rseq1 is convergent_in_cod2
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;
for m being Element of NAT holds ProjMap1 (Rseq1,m) is convergent

proof

let m be Element of NAT ; :: thesis: ProjMap1 (Rseq1,m) is convergent
reconsider m1 = I1 . m as Element of NAT ;
a4: ProjMap1 (Rseq,m1) is convergent by a1;

now :: thesis: for e being Real st 0 < e holds
ex N being Nat st
for n being Nat st n >= N holds
|.(((ProjMap1 (Rseq1,m)) . n) - (lim (ProjMap1 (Rseq,m1)))).| < e

let e be Real; :: thesis: ( 0 < e implies ex N being Nat st
for n being Nat st n >= N holds
|.(((ProjMap1 (Rseq1,m)) . n) - (lim (ProjMap1 (Rseq,m1)))).| < e )
assume 0 < e ; :: thesis: ex N being Nat st
for n being Nat st n >= N holds
|.(((ProjMap1 (Rseq1,m)) . n) - (lim (ProjMap1 (Rseq,m1)))).| < e
then consider N being Nat such that
a5: for n being Nat st n >= N holds
|.(((ProjMap1 (Rseq,m1)) . n) - (lim (ProjMap1 (Rseq,m1)))).| < e by a4, SEQ_2:def 7;
take N = N; :: thesis: for n being Nat st n >= N holds
|.(((ProjMap1 (Rseq1,m)) . n) - (lim (ProjMap1 (Rseq,m1)))).| < e

hereby :: thesis: verum

let n be Nat; :: thesis: ( n >= N implies |.(((ProjMap1 (Rseq1,m)) . n) - (lim (ProjMap1 (Rseq,m1)))).| < e )
assume a6: n >= N ; :: thesis: |.(((ProjMap1 (Rseq1,m)) . n) - (lim (ProjMap1 (Rseq,m1)))).| < e
x2: ( 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 >= N by a6, XXREAL_0:2;
then |.(((ProjMap1 (Rseq,m1)) . (I2 . n)) - (lim (ProjMap1 (Rseq,m1)))).| < e by a5;
then |.((Rseq . ((I1 . m),(I2 . n))) - (lim (ProjMap1 (Rseq,m1)))).| < e by MESFUNC9:def 6;
then |.((Rseq1 . (m,n)) - (lim (ProjMap1 (Rseq,m1)))).| < e by a7;
hence |.(((ProjMap1 (Rseq1,m)) . n) - (lim (ProjMap1 (Rseq,m1)))).| < e by x2, MESFUNC9:def 6; :: thesis: verum

end;

end;

hence ProjMap1 (Rseq1,m) is convergent by SEQ_2:def 6; :: thesis: verum

end;

hence Rseq1 is convergent_in_cod2 ; :: thesis: verum

end;