let f be Function of [:NAT,NAT:],ExtREAL; :: thesis: ( ( for n1, m1, n2, m2 being Nat st n1 <= n2 & m1 <= m2 holds
f . (n1,m1) <= f . (n2,m2) ) implies ( f is P-convergent & P-lim f = sup (rng f) ) )
assume A1: for n1, m1, n2, m2 being Nat st n1 <= n2 & m1 <= m2 holds
f . (n1,m1) <= f . (n2,m2) ; :: thesis: ( f is P-convergent & P-lim f = sup (rng f) )

A2: now :: thesis: for n, m being Nat holds f . (n,m) <= sup (rng f)

let n, m be Nat; :: thesis: f . (n,m) <= sup (rng f)
reconsider n1 = n, m1 = m as Element of NAT by ORDINAL1:def 12;
( [n1,m1] in [:NAT,NAT:] & dom f = [:NAT,NAT:] ) by ZFMISC_1:def 2, FUNCT_2:def 1;
then A3: f . (n1,m1) in rng f by FUNCT_1:def 3;
sup (rng f) is UpperBound of rng f by XXREAL_2:def 3;
hence f . (n,m) <= sup (rng f) by A3, XXREAL_2:def 1; :: thesis: verum

end;

per cases ( for n0, m0 being Nat holds not -infty < f . (n0,m0) or ex n0, m0 being Nat st -infty < f . (n0,m0) ) ;

suppose A4: for n0, m0 being Nat holds not -infty < f . (n0,m0) ; :: thesis: ( f is P-convergent & P-lim f = sup (rng f) )

now :: thesis: for x being ExtReal st x in rng f holds
x <= -infty

let x be ExtReal; :: thesis: ( x in rng f implies x <= -infty )
assume x in rng f ; :: thesis: x <= -infty
then consider z being object such that
B1: ( z in dom f & x = f . z ) by FUNCT_1:def 3;
consider n, m being object such that
B2: ( n in NAT & m in NAT & z = [n,m] ) by B1, ZFMISC_1:def 2;
reconsider n = n, m = m as Nat by B2;
not -infty < f . (n,m) by A4;
hence x <= -infty by B1, B2; :: thesis: verum

end;

then A5: -infty is UpperBound of rng f by XXREAL_2:def 1;
for y being UpperBound of rng f holds -infty <= y by XXREAL_0:5;
then A6: -infty = sup (rng f) by A5, XXREAL_2:def 3;

now :: thesis: for K being Real st K < 0 holds
ex N0 being Nat st
for n, m being Nat st N0 <= n & N0 <= m holds
f . (n,m) <= K

reconsider N0 = 0 as Nat ;
let K be Real; :: thesis: ( K < 0 implies ex N0 being Nat st
for n, m being Nat st N0 <= n & N0 <= m holds
f . (n,m) <= K )
assume K < 0 ; :: thesis: ex N0 being Nat st
for n, m being Nat st N0 <= n & N0 <= m holds
f . (n,m) <= K
take N0 = N0; :: thesis: for n, m being Nat st N0 <= n & N0 <= m holds
f . (n,m) <= K
let n, m be Nat; :: thesis: ( N0 <= n & N0 <= m implies f . (n,m) <= K )
assume ( N0 <= n & N0 <= m ) ; :: thesis: f . (n,m) <= K
f . (n,m) = -infty by A4, XXREAL_0:6;
hence f . (n,m) <= K by XXREAL_0:5; :: thesis: verum

end;

then A7: f is P-convergent_to_-infty ;
then f is P-convergent ;
hence ( f is P-convergent & P-lim f = sup (rng f) ) by A7, A6, Def5; :: thesis: verum

end;

suppose ex n0, m0 being Nat st -infty < f . (n0,m0) ; :: thesis: ( f is P-convergent & P-lim f = sup (rng f) )

then consider n0, m0 being Nat such that
A8: -infty < f . (n0,m0) ;
reconsider n0 = n0, m0 = m0 as Element of NAT by ORDINAL1:def 12;

per cases ( ex K being Real st
for n, m being Nat holds f . (n,m) < K or for K being Real holds
( not 0 < K or ex n, m being Nat st not f . (n,m) < K ) ) ;

suppose ex K being Real st
for n, m being Nat holds f . (n,m) < K ; :: thesis: ( f is P-convergent & P-lim f = sup (rng f) )

then consider K being Real such that
A9: for n, m being Nat holds f . (n,m) < K ;

now :: thesis: for x being ExtReal st x in rng f holds
x <= K

let x be ExtReal; :: thesis: ( x in rng f implies x <= K )
assume x in rng f ; :: thesis: x <= K
then consider z being object such that
C1: ( z in dom f & x = f . z ) by FUNCT_1:def 3;
consider n, m being object such that
C2: ( n in NAT & m in NAT & z = [n,m] ) by C1, ZFMISC_1:def 2;
reconsider n = n, m = m as Nat by C2;
f . (n,m) < K by A9;
hence x <= K by C1, C2; :: thesis: verum

end;

then K is UpperBound of rng f by XXREAL_2:def 1;
then sup (rng f) <= K by XXREAL_2:def 3;
then A11: sup (rng f) <> +infty by XXREAL_0:9, XREAL_0:def 1;
A12: sup (rng f) <> -infty by A2, A8;
then reconsider h = sup (rng f) as Element of REAL by A11, XXREAL_0:14;
A13: for p being Real st 0 < p holds
ex N being Nat st
for n, m being Nat st n >= N & m >= N holds
|.((f . (n,m)) - (sup (rng f))).| < p

proof

let p be Real; :: thesis: ( 0 < p implies ex N being Nat st
for n, m being Nat st n >= N & m >= N holds
|.((f . (n,m)) - (sup (rng f))).| < p )
assume A14: 0 < p ; :: thesis: ex N being Nat st
for n, m being Nat st n >= N & m >= N holds
|.((f . (n,m)) - (sup (rng f))).| < p
reconsider e = p as R_eal by XXREAL_0:def 1;
sup (rng f) in REAL by A12, A11, XXREAL_0:14;
then consider y being ExtReal such that
A15: y in rng f and
A16: (sup (rng f)) - e < y by A14, MEASURE6:6;
consider x being object such that
A17: x in dom f and
A18: y = f . x by A15, FUNCT_1:def 3;
consider i, j being object such that
B1: ( i in NAT & j in NAT & x = [i,j] ) by A17, ZFMISC_1:def 2;
reconsider i = i, j = j as Nat by B1;
reconsider Ni = i, Nj = j as Element of NAT by B1;
set N0 = max (Ni,n0);
set M0 = max (Nj,m0);
set N = max ((max (Ni,n0)),(max (Nj,m0)));
take max ((max (Ni,n0)),(max (Nj,m0))) ; :: thesis: for n, m being Nat st n >= max ((max (Ni,n0)),(max (Nj,m0))) & m >= max ((max (Ni,n0)),(max (Nj,m0))) holds
|.((f . (n,m)) - (sup (rng f))).| < p

hereby :: thesis: verum

let n, m be Nat; :: thesis: ( max ((max (Ni,n0)),(max (Nj,m0))) <= n & max ((max (Ni,n0)),(max (Nj,m0))) <= m implies |.((f . (n,m)) - (sup (rng f))).| < p )
( Ni <= max (Ni,n0) & n0 <= max (Ni,n0) & Nj <= max (Nj,m0) & m0 <= max (Nj,m0) & max (Ni,n0) <= max ((max (Ni,n0)),(max (Nj,m0))) & max (Nj,m0) <= max ((max (Ni,n0)),(max (Nj,m0))) ) by XXREAL_0:25;
then B2: ( Ni <= max ((max (Ni,n0)),(max (Nj,m0))) & Nj <= max ((max (Ni,n0)),(max (Nj,m0))) ) by XXREAL_0:2;
assume ( max ((max (Ni,n0)),(max (Nj,m0))) <= n & max ((max (Ni,n0)),(max (Nj,m0))) <= m ) ; :: thesis: |.((f . (n,m)) - (sup (rng f))).| < p
then ( Ni <= n & Nj <= m ) by B2, XXREAL_0:2;
then f . (Ni,Nj) <= f . (n,m) by A1;
then (sup (rng f)) - e < f . (n,m) by A16, A18, B1, XXREAL_0:2;
then sup (rng f) < (f . (n,m)) + e by XXREAL_3:54;
then (sup (rng f)) - (f . (n,m)) < e by XXREAL_3:55;
then - e < - ((sup (rng f)) - (f . (n,m))) by XXREAL_3:38;
then A20: - e < (f . (n,m)) - (sup (rng f)) by XXREAL_3:26;
A21: f . (n,m) <= sup (rng f) by A2;

A22: now :: thesis: not sup (rng f) = (sup (rng f)) + e

assume A23: sup (rng f) = (sup (rng f)) + e ; :: thesis: contradiction
(e + (sup (rng f))) + (- (sup (rng f))) = e + ((sup (rng f)) + (- (sup (rng f)))) by A12, A11, XXREAL_3:29
.= e + 0 by XXREAL_3:7
.= e by XXREAL_3:4 ;
hence contradiction by A14, A23, XXREAL_3:7; :: thesis: verum

end;

(sup (rng f)) + 0 <= (sup (rng f)) + e by A14, XXREAL_3:36;
then sup (rng f) <= (sup (rng f)) + e by XXREAL_3:4;
then sup (rng f) < (sup (rng f)) + e by A22, XXREAL_0:1;
then f . (n,m) < (sup (rng f)) + e by A21, XXREAL_0:2;
then (f . (n,m)) - (sup (rng f)) < e by XXREAL_3:55;
hence |.((f . (n,m)) - (sup (rng f))).| < p by A20, EXTREAL1:22; :: thesis: verum

end;

end;

A24: h = sup (rng f) ;
then A25: f is P-convergent_to_finite_number by A13;
hence f is P-convergent ; :: thesis: P-lim f = sup (rng f)
hence P-lim f = sup (rng f) by A13, A24, A25, Def5; :: thesis: verum

end;

suppose A26: for K being Real holds
( not 0 < K or ex n, m being Nat st not f . (n,m) < K ) ; :: thesis: ( f is P-convergent & P-lim f = sup (rng f) )

now :: thesis: for K being Real st 0 < K holds
ex N being Nat st
for n, m being Nat st N <= n & N <= m holds
K <= f . (n,m)

let K be Real; :: thesis: ( 0 < K implies ex N being Nat st
for n, m being Nat st N <= n & N <= m holds
K <= f . (n,m) )
assume 0 < K ; :: thesis: ex N being Nat st
for n, m being Nat st N <= n & N <= m holds
K <= f . (n,m)
then consider N0, N1 being Nat such that
A27: K <= f . (N0,N1) by A26;
reconsider n0 = N0, n1 = N1 as Element of NAT by ORDINAL1:def 12;
set N = max (n0,n1);
B3: ( max (n0,n1) >= N0 & max (n0,n1) >= N1 ) by XXREAL_0:25;
reconsider N = max (n0,n1) as Nat ;

now :: thesis: for n, m being Nat st N <= n & N <= m holds
K <= f . (n,m)

let n, m be Nat; :: thesis: ( N <= n & N <= m implies K <= f . (n,m) )
assume ( N <= n & N <= m ) ; :: thesis: K <= f . (n,m)
then ( N0 <= n & N1 <= m ) by B3, XXREAL_0:2;
then f . (N0,N1) <= f . (n,m) by A1;
hence K <= f . (n,m) by A27, XXREAL_0:2; :: thesis: verum

end;

hence ex N being Nat st
for n, m being Nat st N <= n & N <= m holds
K <= f . (n,m) ; :: thesis: verum

end;

then A28: f is P-convergent_to_+infty ;
hence A29: f is P-convergent ; :: thesis: P-lim f = sup (rng f)

now :: thesis: not sup (rng f) <> +infty

assume A30: sup (rng f) <> +infty ; :: thesis: contradiction
f . (n0,m0) <= sup (rng f) by A2;
then reconsider h = sup (rng f) as Element of REAL by A8, A30, XXREAL_0:14;
set K = max (0,h);
0 <= max (0,h) by XXREAL_0:25;
then consider N0, M0 being Nat such that
A31: (max (0,h)) + 1 <= f . (N0,M0) by A26;
h + 0 < (max (0,h)) + 1 by XREAL_1:8, XXREAL_0:25;
then sup (rng f) < f . (N0,M0) by A31, XXREAL_0:2;
hence contradiction by A2; :: thesis: verum

end;

hence P-lim f = sup (rng f) by A28, A29, Def5; :: thesis: verum

end;

end;

end;

end;