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

hereby :: thesis: verum

let Rseq1 be subsequence of Rseq; :: thesis: Rseq1 is convergent_in_cod1
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 ProjMap2 (Rseq1,m) is convergent

proof

let m be Element of NAT ; :: thesis: ProjMap2 (Rseq1,m) is convergent
reconsider m2 = I2 . m as Element of NAT ;
a4: ProjMap2 (Rseq,m2) 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
|.(((ProjMap2 (Rseq1,m)) . n) - (lim (ProjMap2 (Rseq,m2)))).| < e

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

hereby :: thesis: verum

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

end;

end;

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

end;

hence Rseq1 is convergent_in_cod1 ; :: thesis: verum

end;