let f be Function of [:NAT,NAT:],ExtREAL; :: thesis: ( f is P-convergent_to_-infty implies ( not f is P-convergent_to_+infty & not f is P-convergent_to_finite_number ) )
assume A1: f is P-convergent_to_-infty ; :: thesis: ( not f is P-convergent_to_+infty & not f is P-convergent_to_finite_number )

hereby :: thesis: not f is P-convergent_to_finite_number

assume f is P-convergent_to_+infty ; :: thesis: contradiction
then consider N1 being Nat such that
A3: for n, m being Nat st n >= N1 & m >= N1 holds
f . (n,m) >= 1 ;
consider N2 being Nat such that
A4: for n, m being Nat st n >= N2 & m >= N2 holds
- 1 >= f . (n,m) by A1;
reconsider N1 = N1, N2 = N2 as Element of NAT by ORDINAL1:def 12;
set N = max (N1,N2);
A5: ( max (N1,N2) >= N1 & max (N1,N2) >= N2 ) by XXREAL_0:25;
then f . ((max (N1,N2)),(max (N1,N2))) >= 1 by A3;
hence contradiction by A4, A5; :: thesis: verum

end;

assume f is P-convergent_to_finite_number ; :: thesis: contradiction
then consider p being Real such that
A6: for e being Real st 0 < e holds
ex N being Nat st
for n, m being Nat st n >= N & m >= N holds
|.((f . (n,m)) - p).| < e ;
reconsider p1 = p as ExtReal ;

per cases ( p > 0 or p = 0 or p < 0 ) ;

suppose A9: p > 0 ; :: thesis: contradiction

then consider N1 being Nat such that
A7: for n, m being Nat st n >= N1 & m >= N1 holds
|.((f . (n,m)) - p1).| < p by A6;

A8: now :: thesis: for n, m being Nat st n >= N1 & m >= N1 holds
0 < f . (n,m)

let n, m be Nat; :: thesis: ( n >= N1 & m >= N1 implies 0 < f . (n,m) )
assume ( n >= N1 & m >= N1 ) ; :: thesis: 0 < f . (n,m)
then |.((f . (n,m)) - p).| < p by A7;
then - p1 < (f . (n,m)) - p by EXTREAL1:21;
then (- p1) + p < f . (n,m) by XXREAL_3:53;
hence 0 < f . (n,m) by XXREAL_3:7; :: thesis: verum

end;

consider N2 being Nat such that
A10: for n, m being Nat st n >= N2 & m >= N2 holds
- (2 * p) >= f . (n,m) by A1, A9;
reconsider N1 = N1, N2 = N2 as Element of NAT by ORDINAL1:def 12;
set N = max (N1,N2);
A11: ( max (N1,N2) >= N1 & max (N1,N2) >= N2 ) by XXREAL_0:25;
then 0 < f . ((max (N1,N2)),(max (N1,N2))) by A8;
hence contradiction by A9, A11, A10; :: thesis: verum

end;

suppose A12: p = 0 ; :: thesis: contradiction

consider N1 being Nat such that
A13: for n, m being Nat st n >= N1 & m >= N1 holds
|.((f . (n,m)) - p).| < 1 by A6;
consider N2 being Nat such that
A14: for n, m being Nat st n >= N2 & m >= N2 holds
- 1 >= f . (n,m) by A1;
reconsider N1 = N1, N2 = N2 as Element of NAT by ORDINAL1:def 12;
reconsider jj = 1 as ExtReal ;
set N = max (N1,N2);
A15: ( max (N1,N2) >= N1 & max (N1,N2) >= N2 ) by XXREAL_0:25;
then |.((f . ((max (N1,N2)),(max (N1,N2)))) - p1).| < jj by A13;
then - jj < (f . ((max (N1,N2)),(max (N1,N2)))) - p1 by EXTREAL1:21;
then (- jj) + p < f . ((max (N1,N2)),(max (N1,N2))) by XXREAL_3:53;
then - jj < f . ((max (N1,N2)),(max (N1,N2))) by A12, XXREAL_3:4;
then - 1 < f . ((max (N1,N2)),(max (N1,N2))) by XXREAL_3:def 3;
hence contradiction by A14, A15; :: thesis: verum

end;

suppose A16: p < 0 ; :: thesis: contradiction

then consider N1 being Nat such that
A17: for n, m being Nat st n >= N1 & m >= N1 holds
|.((f . (n,m)) - p).| < - p by A6;

A18: now :: thesis: for n, m being Nat st n >= N1 & m >= N1 holds
2 * p < f . (n,m)

let n, m be Nat; :: thesis: ( n >= N1 & m >= N1 implies 2 * p < f . (n,m) )
assume ( n >= N1 & m >= N1 ) ; :: thesis: 2 * p < f . (n,m)
then |.((f . (n,m)) - p).| < - p by A17;
then - (- p1) < (f . (n,m)) - p1 by EXTREAL1:21;
then p1 + p1 < f . (n,m) by XXREAL_3:53;
then 2 * p1 < f . (n,m) by XXREAL_3:94;
hence 2 * p < f . (n,m) by XXREAL_3:def 5; :: thesis: verum

end;

consider N2 being Nat such that
A19: for n, m being Nat st n >= N2 & m >= N2 holds
f . (n,m) <= 2 * p by A1, A16;
reconsider N1 = N1, N2 = N2 as Element of NAT by ORDINAL1:def 12;
set N = max (N1,N2);
A20: ( max (N1,N2) >= N1 & max (N1,N2) >= N2 ) by XXREAL_0:25;
then 2 * p < f . ((max (N1,N2)),(max (N1,N2))) by A18;
hence contradiction by A19, A20; :: thesis: verum

end;

end;