let Rseq be Function of [:NAT,NAT:],REAL; ( 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 )
; for n, m being Nat holds Rseq . (n,m) <= P-lim Rseq
hereby verum
let n,
m be
Nat;
Rseq . (n,m) <= P-lim Rseqreconsider 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 H1(
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)
= H1(
i,
j)
from BINOP_1:sch 4();
a5:
now for i, j being Nat holds Rseq1 . (i,j) <= Rseq2 . (i,j)let i,
j be
Nat;
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;
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 H2(
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 = H2(
i)
from FUNCT_2:sch 4();
then reconsider N =
N as
V113()
sequence of
NAT by VALUED_1:def 13;
deffunc H3(
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 = H3(
j)
from FUNCT_2:sch 4();
then reconsider M =
M as
V113()
sequence of
NAT by VALUED_1:def 13;
for
i,
j being
Nat holds
Rseq2 . (
i,
j)
= Rseq . (
(N . i),
(M . j))
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;
verum
end;