let Rseq be Function of [:NAT,NAT:],REAL; :: thesis: ( Rseq is non-decreasing & Rseq is P-convergent implies for n, m being Nat holds Rseq . (n,m) <= P-lim Rseq )
assume a1: ( Rseq is non-decreasing & Rseq is P-convergent ) ; :: thesis: for n, m being Nat holds Rseq . (n,m) <= P-lim Rseq

hereby :: thesis: verum

let n, m be Nat; :: thesis: Rseq . (n,m) <= P-lim Rseq
reconsider n1 = n, m1 = m as Element of NAT by ORDINAL1:def 12;
Rseq . (n,m) is Element of REAL by XREAL_0:def 1;
then reconsider Rseq1 = [:NAT,NAT:] --> (Rseq . (n,m)) as Function of [:NAT,NAT:],REAL by FUNCOP_1:46;
deffunc H₁( Element of NAT , Element of NAT ) -> Element of REAL = Rseq . ((n + $1),(m + $2));
consider Rseq2 being Function of [:NAT,NAT:],REAL such that
a4: for i, j being Element of NAT holds Rseq2 . (i,j) = H₁(i,j) from BINOP_1:sch 4();

a5: now :: thesis: for i, j being Nat holds Rseq1 . (i,j) <= Rseq2 . (i,j)

let i, j be Nat; :: thesis: Rseq1 . (i,j) <= Rseq2 . (i,j)
a6: ( n + i >= n & m + j >= m ) by NAT_1:11;
( i in NAT & j in NAT ) by ORDINAL1:def 12;
then ( Rseq1 . (i,j) = Rseq . (n,m) & Rseq2 . (i,j) = Rseq . ((n + i),(m + j)) ) by a4, FUNCOP_1:70;
hence Rseq1 . (i,j) <= Rseq2 . (i,j) by a1, a6; :: thesis: verum

end;

reconsider r = Rseq . (n,m) as Element of REAL by XREAL_0:def 1;
Rseq1 = [:NAT,NAT:] --> r ;
then a7: ( Rseq1 is P-convergent & P-lim Rseq1 = Rseq . (n,m) ) by DBLSEQ_1:2;
deffunc H₂( Element of NAT ) -> Element of omega = n + $1;
consider N being Function of NAT,NAT such that
b1: for i being Element of NAT holds N . i = H₂(i) from FUNCT_2:sch 4();

now :: thesis: for k being Nat holds N . k < N . (k + 1)

let k be Nat; :: thesis: N . k < N . (k + 1)
k is Element of NAT by ORDINAL1:def 12;
then b2: ( N . k = n + k & N . (k + 1) = n + (k + 1) ) by b1;
k < k + 1 by NAT_1:13;
hence N . k < N . (k + 1) by b2, XREAL_1:6; :: thesis: verum

end;

then reconsider N = N as increasing sequence of NAT by VALUED_1:def 13;
deffunc H₃( Element of NAT ) -> Element of omega = m + $1;
consider M being Function of NAT,NAT such that
c1: for j being Element of NAT holds M . j = H₃(j) from FUNCT_2:sch 4();

now :: thesis: for k being Nat holds M . k < M . (k + 1)

let k be Nat; :: thesis: M . k < M . (k + 1)
k is Element of NAT by ORDINAL1:def 12;
then c2: ( M . k = m + k & M . (k + 1) = m + (k + 1) ) by c1;
k < k + 1 by NAT_1:13;
hence M . k < M . (k + 1) by c2, XREAL_1:6; :: thesis: verum

end;

then reconsider M = M as increasing sequence of NAT by VALUED_1:def 13;
for i, j being Nat holds Rseq2 . (i,j) = Rseq . ((N . i),(M . j))

proof

let i, j be Nat; :: thesis: Rseq2 . (i,j) = Rseq . ((N . i),(M . j))
c5: ( i in NAT & j in NAT ) by ORDINAL1:def 12;
then ( N . i = n + i & M . j = m + j ) by b1, c1;
hence Rseq2 . (i,j) = Rseq . ((N . i),(M . j)) by c5, a4; :: thesis: verum

end;

then Rseq2 is subsequence of Rseq by DBLSEQ_1:def 14;
then ( Rseq2 is P-convergent & P-lim Rseq2 = P-lim Rseq ) by a1, DBLSEQ_1:17;
hence Rseq . (n,m) <= P-lim Rseq by a5, a7, DBLSEQ_1:15; :: thesis: verum

end;