let Rseq be 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 )
let Rseq1 be subsequence of Rseq; ( 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 )
; ( lim_in_cod2 Rseq1 is convergent & cod2_major_iterated_lim Rseq1 = cod2_major_iterated_lim Rseq )
consider I1, I2 being V113() 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;
( 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
;
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
;
for m being Nat st m >= N holds
|.(((lim_in_cod2 Rseq1) . m) - (cod2_major_iterated_lim Rseq)).| < e
hereby verum
let m be
Nat;
( 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
;
|.(((lim_in_cod2 Rseq1) . m) - (cod2_major_iterated_lim Rseq)).| < ereconsider 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;
( 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
;
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
;
for n being Nat st n >= K holds
|.(((ProjMap1 (Rseq1,mm)) . n) - (lim (ProjMap1 (Rseq,m1)))).| < p
hereby verum
let n be
Nat;
( n >= K implies |.(((ProjMap1 (Rseq1,mm)) . n) - (lim (ProjMap1 (Rseq,m1)))).| < p )assume b3:
n >= K
;
|.(((ProjMap1 (Rseq1,mm)) . n) - (lim (ProjMap1 (Rseq,m1)))).| < px3:
(
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;
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;
verum
end;
end;
hence
lim_in_cod2 Rseq1 is convergent
by SEQ_2:def 6; cod2_major_iterated_lim Rseq1 = cod2_major_iterated_lim Rseq
hence
cod2_major_iterated_lim Rseq1 = cod2_major_iterated_lim Rseq
by a10, def35; verum