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
f . (n,m) < 2 * p

let n, m be Nat; :: thesis: ( n >= N1 & m >= N1 implies f . (n,m) < 2 * p )
assume ( n >= N1 & m >= N1 ) ; :: thesis: f . (n,m) < 2 * p
then |.((f . (n,m)) - p).| < p by A7;
then (f . (n,m)) - p1 < p by EXTREAL1:21;
then f . (n,m) < p1 + p1 by XXREAL_3:54;
then f . (n,m) < 2 * p1 by XXREAL_3:94;
hence f . (n,m) < 2 * p by XXREAL_3:def 5; :: 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 f . ((max (N1,N2)),(max (N1,N2))) < 2 * p by A8;
hence contradiction by 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 (f . ((max (N1,N2)),(max (N1,N2)))) - p1 < jj by EXTREAL1:21;
then f . ((max (N1,N2)),(max (N1,N2))) < jj + p1 by XXREAL_3:54;
then f . ((max (N1,N2)),(max (N1,N2))) < 1 + 0 by A12, XXREAL_3:def 2;
hence contradiction by A14, A15; :: thesis: verum

end;

suppose 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
f . (n,m) < 0

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

end;

consider N2 being Nat such that
A19: 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);
A20: ( max (N1,N2) >= N1 & max (N1,N2) >= N2 ) by XXREAL_0:25;
then f . ((max (N1,N2)),(max (N1,N2))) < 0 by A18;
hence contradiction by A19, A20; :: thesis: verum

end;

end;