let Rseq be Function of [:NAT,NAT:],REAL; :: thesis: ( Rseq is uniformly_convergent_in_cod1 & lim_in_cod1 Rseq is convergent implies ( Rseq is P-convergent & P-lim Rseq = cod1_major_iterated_lim Rseq ) )
assume that
a3: Rseq is uniformly_convergent_in_cod1 and
a2: lim_in_cod1 Rseq is convergent ; :: thesis: ( Rseq is P-convergent & P-lim Rseq = cod1_major_iterated_lim Rseq )
a4: now :: thesis: for e being Real st 0 < e holds
ex N being Nat st
for n, m being Nat st n >= N & m >= N holds
|.((Rseq . (n,m)) - (cod1_major_iterated_lim Rseq)).| < e
let e be Real; :: thesis: ( 0 < e implies ex N being Nat st
for n, m being Nat st n >= N & m >= N holds
|.((Rseq . (n,m)) - (cod1_major_iterated_lim Rseq)).| < e )
assume a5: 0 < e ; :: thesis: ex N being Nat st
for n, m being Nat st n >= N & m >= N holds
|.((Rseq . (n,m)) - (cod1_major_iterated_lim Rseq)).| < e
then consider N1 being Nat such that
a6: for m being Nat st m >= N1 holds
for n being Nat holds |.((Rseq . (n,m)) - ((lim_in_cod1 Rseq) . n)).| < e / 2 by a3;
consider z being Real such that
a7: for e being Real st e > 0 holds
ex N2 being Nat st
for m being Nat st m >= N2 holds
|.(((lim_in_cod1 Rseq) . m) - z).| < e by a2, SEQ_2:def 6;
a8: z = cod1_major_iterated_lim Rseq by a2, a7, def34;
consider N2 being Nat such that
a9: for n being Nat st n >= N2 holds
|.(((lim_in_cod1 Rseq) . n) - z).| < e / 2 by a5, a7;
set N = max (N1,N2);
a0: max (N1,N2) is Nat by TARSKI:1;
for n, m being Nat st n >= max (N1,N2) & m >= max (N1,N2) holds
|.((Rseq . (n,m)) - (cod1_major_iterated_lim Rseq)).| < e
proof
let n, m be Nat; :: thesis: ( n >= max (N1,N2) & m >= max (N1,N2) implies |.((Rseq . (n,m)) - (cod1_major_iterated_lim Rseq)).| < e )
assume a10: ( n >= max (N1,N2) & m >= max (N1,N2) ) ; :: thesis: |.((Rseq . (n,m)) - (cod1_major_iterated_lim Rseq)).| < e
( max (N1,N2) >= N1 & max (N1,N2) >= N2 ) by XXREAL_0:25;
then ( n >= N2 & m >= N1 ) by a10, XXREAL_0:2;
then ( |.((Rseq . (n,m)) - ((lim_in_cod1 Rseq) . n)).| < e / 2 & |.(((lim_in_cod1 Rseq) . n) - z).| < e / 2 ) by a6, a9;
then a12: |.((Rseq . (n,m)) - ((lim_in_cod1 Rseq) . n)).| + |.(((lim_in_cod1 Rseq) . n) - z).| < (e / 2) + (e / 2) by XREAL_1:8;
|.((Rseq . (n,m)) - (cod1_major_iterated_lim Rseq)).| <= |.((Rseq . (n,m)) - ((lim_in_cod1 Rseq) . n)).| + |.(((lim_in_cod1 Rseq) . n) - (cod1_major_iterated_lim Rseq)).| by COMPLEX1:63;
hence |.((Rseq . (n,m)) - (cod1_major_iterated_lim Rseq)).| < e by a8, a12, XXREAL_0:2; :: thesis: verum
end;
hence ex N being Nat st
for n, m being Nat st n >= N & m >= N holds
|.((Rseq . (n,m)) - (cod1_major_iterated_lim Rseq)).| < e by a0; :: thesis: verum
end;
hence Rseq is P-convergent ; :: thesis: P-lim Rseq = cod1_major_iterated_lim Rseq
hence P-lim Rseq = cod1_major_iterated_lim Rseq by a4, def6; :: thesis: verum