let Rseq be Function of [:NAT,NAT:],REAL; :: thesis: ( Rseq is P-convergent & Rseq is convergent_in_cod1 implies P-lim Rseq = cod1_major_iterated_lim Rseq )
assume a1: ( Rseq is P-convergent & Rseq is convergent_in_cod1 ) ; :: thesis: P-lim Rseq = cod1_major_iterated_lim Rseq
then consider z being Real such that
a3: for e being Real st 0 < e holds
ex N1 being Nat st
for n, m being Nat st n >= N1 & m >= N1 holds
|.((Rseq . (n,m)) - z).| < e ;
for e being Real st 0 < e holds
ex N being Nat st
for n being Nat st n >= N holds
|.(((lim_in_cod1 Rseq) . n) - z).| < e

proof

let e be Real; :: thesis: ( 0 < e implies ex N being Nat st
for n being Nat st n >= N holds
|.(((lim_in_cod1 Rseq) . n) - z).| < e )
assume a8: 0 < e ; :: thesis: ex N being Nat st
for n being Nat st n >= N holds
|.(((lim_in_cod1 Rseq) . n) - z).| < e
then consider N1 being Nat such that
a15: for n, m being Nat st n >= N1 & m >= N1 holds
|.((Rseq . (n,m)) - z).| < e / 2 by a3;
a12: for n being Element of NAT st n >= N1 holds
ex N2 being Nat st
for m being Nat st m >= N2 holds
|.(((ProjMap2 (Rseq,n)) . m) - ((lim_in_cod1 Rseq) . n)).| < e / 2

proof

let n be Element of NAT ; :: thesis: ( n >= N1 implies ex N2 being Nat st
for m being Nat st m >= N2 holds
|.(((ProjMap2 (Rseq,n)) . m) - ((lim_in_cod1 Rseq) . n)).| < e / 2 )
assume n >= N1 ; :: thesis: ex N2 being Nat st
for m being Nat st m >= N2 holds
|.(((ProjMap2 (Rseq,n)) . m) - ((lim_in_cod1 Rseq) . n)).| < e / 2
ProjMap2 (Rseq,n) is convergent by a1;
then consider N2 being Nat such that
a9: for m being Nat st m >= N2 holds
|.(((ProjMap2 (Rseq,n)) . m) - (lim (ProjMap2 (Rseq,n)))).| < e / 2 by a8, SEQ_2:def 7;
take N2 ; :: thesis: for m being Nat st m >= N2 holds
|.(((ProjMap2 (Rseq,n)) . m) - ((lim_in_cod1 Rseq) . n)).| < e / 2
thus for m being Nat st m >= N2 holds
|.(((ProjMap2 (Rseq,n)) . m) - ((lim_in_cod1 Rseq) . n)).| < e / 2 :: thesis: verum

proof

let m be Nat; :: thesis: ( m >= N2 implies |.(((ProjMap2 (Rseq,n)) . m) - ((lim_in_cod1 Rseq) . n)).| < e / 2 )
assume m >= N2 ; :: thesis: |.(((ProjMap2 (Rseq,n)) . m) - ((lim_in_cod1 Rseq) . n)).| < e / 2
then |.(((ProjMap2 (Rseq,n)) . m) - (lim (ProjMap2 (Rseq,n)))).| < e / 2 by a9;
hence |.(((ProjMap2 (Rseq,n)) . m) - ((lim_in_cod1 Rseq) . n)).| < e / 2 by def32; :: thesis: verum

end;

end;

take N1 ; :: thesis: for n being Nat st n >= N1 holds
|.(((lim_in_cod1 Rseq) . n) - z).| < e
thus for n being Nat st n >= N1 holds
|.(((lim_in_cod1 Rseq) . n) - z).| < e :: thesis: verum

proof

let n be Nat; :: thesis: ( n >= N1 implies |.(((lim_in_cod1 Rseq) . n) - z).| < e )
reconsider n1 = n as Element of NAT by ORDINAL1:def 12;
assume a14: n >= N1 ; :: thesis: |.(((lim_in_cod1 Rseq) . n) - z).| < e
then consider N2 being Nat such that
a13: for m being Nat st m >= N2 holds
|.(((ProjMap2 (Rseq,n1)) . m) - ((lim_in_cod1 Rseq) . n)).| < e / 2 by a12;
reconsider M = max (N2,N1) as Element of NAT by ORDINAL1:def 12;
a17: (ProjMap2 (Rseq,n1)) . M = Rseq . (M,n) by MESFUNC9:def 7;
a16: ( M >= N2 & M >= N1 ) by XXREAL_0:25;
a18: |.(((lim_in_cod1 Rseq) . n) - z).| <= |.(((lim_in_cod1 Rseq) . n) - ((ProjMap2 (Rseq,n1)) . M)).| + |.((Rseq . (M,n)) - z).| by a17, COMPLEX1:63;
|.(((lim_in_cod1 Rseq) . n) - ((ProjMap2 (Rseq,n1)) . M)).| = |.(((ProjMap2 (Rseq,n1)) . M) - ((lim_in_cod1 Rseq) . n)).| by COMPLEX1:60;
then a20: |.(((lim_in_cod1 Rseq) . n) - ((ProjMap2 (Rseq,n1)) . M)).| < e / 2 by a13, XXREAL_0:25;
|.((Rseq . (M,n1)) - z).| < e / 2 by a15, a16, a14;
then |.(((lim_in_cod1 Rseq) . n) - ((ProjMap2 (Rseq,n1)) . M)).| + |.((Rseq . (M,n)) - z).| < (e / 2) + (e / 2) by a20, XREAL_1:8;
hence |.(((lim_in_cod1 Rseq) . n) - z).| < e by a18, XXREAL_0:2; :: thesis: verum

end;

end;

then a21: lim_in_cod1 Rseq is convergent by SEQ_2:def 6;
for e being Real st 0 < e holds
ex N being Nat st
for n being Nat st n >= N holds
|.(((lim_in_cod1 Rseq) . n) - (P-lim Rseq)).| < e

proof

let e be Real; :: thesis: ( 0 < e implies ex N being Nat st
for n being Nat st n >= N holds
|.(((lim_in_cod1 Rseq) . n) - (P-lim Rseq)).| < e )
assume a22: 0 < e ; :: thesis: ex N being Nat st
for n being Nat st n >= N holds
|.(((lim_in_cod1 Rseq) . n) - (P-lim Rseq)).| < e
then consider N1 being Nat such that
a23: for n, m being Nat st n >= N1 & m >= N1 holds
|.((Rseq . (n,m)) - (P-lim Rseq)).| < e / 2 by a1, def6;
take N = N1; :: thesis: for n being Nat st n >= N holds
|.(((lim_in_cod1 Rseq) . n) - (P-lim Rseq)).| < e

hereby :: thesis: verum

let n be Nat; :: thesis: ( n >= N implies |.(((lim_in_cod1 Rseq) . n) - (P-lim Rseq)).| < e )
assume n >= N ; :: thesis: |.(((lim_in_cod1 Rseq) . n) - (P-lim Rseq)).| < e
then a27: for m being Nat st m >= N1 holds
|.((Rseq . (m,n)) - (P-lim Rseq)).| < e / 2 by a23;
reconsider n1 = n as Element of NAT by ORDINAL1:def 12;
ProjMap2 (Rseq,n1) is convergent by a1;
then consider N3 being Nat such that
a29: for m being Nat st m >= N3 holds
|.(((ProjMap2 (Rseq,n1)) . m) - (lim (ProjMap2 (Rseq,n1)))).| < e / 2 by a22, SEQ_2:def 7;
reconsider M = max (N1,N3) as Element of NAT by ORDINAL1:def 12;
a31: |.((Rseq . (M,n)) - (P-lim Rseq)).| < e / 2 by a27, XXREAL_0:25;
(ProjMap2 (Rseq,n1)) . M = Rseq . (M,n) by MESFUNC9:def 7;
then |.((Rseq . (M,n)) - (lim (ProjMap2 (Rseq,n1)))).| < e / 2 by a29, XXREAL_0:25;
then |.((Rseq . (M,n)) - ((lim_in_cod1 Rseq) . n)).| < e / 2 by def32;
then |.(((lim_in_cod1 Rseq) . n) - (Rseq . (M,n))).| < e / 2 by COMPLEX1:60;
then a32: |.(((lim_in_cod1 Rseq) . n) - (Rseq . (M,n))).| + |.((Rseq . (M,n)) - (P-lim Rseq)).| < (e / 2) + (e / 2) by a31, XREAL_1:8;
|.(((lim_in_cod1 Rseq) . n) - (P-lim Rseq)).| <= |.(((lim_in_cod1 Rseq) . n) - (Rseq . (M,n))).| + |.((Rseq . (M,n)) - (P-lim Rseq)).| by COMPLEX1:63;
hence |.(((lim_in_cod1 Rseq) . n) - (P-lim Rseq)).| < e by a32, XXREAL_0:2; :: thesis: verum

end;

end;

hence P-lim Rseq = cod1_major_iterated_lim Rseq by a21, def34; :: thesis: verum