let Rseq be Function of [:NAT,NAT:],REAL; :: thesis:
assume a1: ( Rseq is non-decreasing & Rseq is P-convergent ) ; :: thesis:
then consider p being Real such that
a3: 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)) - p).| < e ;
consider N being Nat such that
a4: for n, m being Nat st n >= N & m >= N holds
|.((Rseq . (n,m)) - p).| < 1 by a3;
a5: for n, m being Nat st n >= N & m >= N holds
|.(Rseq . (n,m)).| < 1 + |.p.|

let n, m be Nat; :: thesis:
assume ( n >= N & m >= N ) ; :: thesis:
then a6: |.((Rseq . (n,m)) - p).| < 1 by a4;
|.((Rseq . (n,m)) - p).| >= |.(Rseq . (n,m)).| - |.p.| by COMPLEX1:59;
then |.(Rseq . (n,m)).| - |.p.| < 1 by a6, XXREAL_0:2;
hence |.(Rseq . (n,m)).| < 1 + |.p.| by XREAL_1:19; :: thesis:

end;

deffunc H₁( Element of NAT ) -> Element of NAT = c₁;
deffunc H₂( Nat) -> object = |.(Rseq . (1,c₁)).|;
reconsider E2 = { H₁(m) where m is Element of NAT : m <= N } as non empty finite Subset of NAT from ASYMPT_0:sch 2();
reconsider EE = [:E2,E2:] as finite set ;
c1: E2 is finite ;
deffunc H₃( Element of NAT , Element of NAT ) -> object = |.(Rseq . (c₁,c₂)).|;
a9: { H₃(m,n) where m, n is Element of NAT : ( m in E2 & n in E2 ) } is finite from FRAENKEL:sch 22(c1, c1);
set F = { H₃(m,n) where m, n is Element of NAT : ( m in E2 & n in E2 ) } ;
N is Element of NAT by ORDINAL1:def 12;
then N in E2 ;
then b1: |.(Rseq . (N,N)).| in { H₃(m,n) where m, n is Element of NAT : ( m in E2 & n in E2 ) } ;

let x be object ; :: thesis:
assume x in { H₃(m,n) where m, n is Element of NAT : ( m in E2 & n in E2 ) } ; :: thesis:
then consider p, q being Element of NAT such that
a10: ( x = H₃(p,q) & p in E2 & q in E2 ) ;
thus x is real by a10; :: thesis:

end;

then reconsider F = { H₃(m,n) where m, n is Element of NAT : ( m in E2 & n in E2 ) } as non empty real-membered set by b1, MEMBERED:def 3;
reconsider M1 = sup F as Element of REAL by a9, XXREAL_2:16;
set M = max (M1,(1 + |.p.|));
a14: ( max (M1,(1 + |.p.|)) >= 1 + |.p.| & 1 + |.p.| >= 1 & max (M1,(1 + |.p.|)) >= M1 & max (M1,(1 + |.p.|)) >= M1 ) by XXREAL_0:25, XREAL_1:31, COMPLEX1:46;
c1: for n, m being Nat holds |.(Rseq . (n,m)).| <= max (M1,(1 + |.p.|))

end;

end;

end;

end;

end;

end;

let a be ExtReal; :: thesis:
assume a in Rseq .: [:NAT,NAT:] ; :: thesis:
then consider x being Element of [:NAT,NAT:] such that
b2: ( x in [:NAT,NAT:] & a = Rseq . x ) by FUNCT_2:65;
consider n, m being object such that
b3: ( n in NAT & m in NAT & x = [n,m] ) by ZFMISC_1:def 2;
reconsider n = n, m = m as Element of NAT by b3;
|.(Rseq . (n,m)).| <= max (M1,(1 + |.p.|)) by c1;
hence ( - (max (M1,(1 + |.p.|))) <= a & a <= max (M1,(1 + |.p.|)) ) by b2, b3, ABSVALUE:5; :: thesis:

end;