let f be PartFunc of REAL,REAL; :: thesis: ( f is divergent_in+infty_to+infty implies ( not f is convergent_in+infty & not f is divergent_in+infty_to-infty ) )
assume A1: f is divergent_in+infty_to+infty ; :: thesis: ( not f is convergent_in+infty & not f is divergent_in+infty_to-infty )

hereby :: thesis: not f is divergent_in+infty_to-infty

assume f is convergent_in+infty ; :: thesis: contradiction
then consider g being Real such that
A2: for g1 being Real st 0 < g1 holds
ex r being Real st
for r1 being Real st r < r1 & r1 in dom f holds
|.((f . r1) - g).| < g1 by LIMFUNC1:44;
consider R1 being Real such that
A3: for r1 being Real st R1 < r1 & r1 in dom f holds
|.((f . r1) - g).| < 1 by A2;
consider R2 being Real such that
A4: for r1 being Real st R2 < r1 & r1 in dom f holds
g + 1 < f . r1 by A1, LIMFUNC1:46;
set R = max (R1,R2);
A5: ( max (R1,R2) >= R1 & max (R1,R2) >= R2 ) by XXREAL_0:25;
consider r being Real such that
A6: ( r > max (R1,R2) & r in dom f ) by A1, LIMFUNC1:46;
A7: r > R1 by A5, A6, XXREAL_0:2;
r > R2 by A5, A6, XXREAL_0:2;
then g + 1 < f . r by A4, A6;
then A8: 1 < (f . r) - g by XREAL_1:20;
(f . r) - g <= |.((f . r) - g).| by ABSVALUE:4;
then 1 < |.((f . r) - g).| by A8, XXREAL_0:2;
hence contradiction by A3, A6, A7; :: thesis: verum

end;

hereby :: thesis: verum

assume f is divergent_in+infty_to-infty ; :: thesis: contradiction
then consider R1 being Real such that
A9: for r1 being Real st r1 > R1 & r1 in dom f holds
f . r1 < 0 by LIMFUNC1:47;
consider R2 being Real such that
A10: for r1 being Real st r1 > R2 & r1 in dom f holds
0 < f . r1 by A1, LIMFUNC1:46;
set R = max (R1,R2);
A11: ( max (R1,R2) >= R1 & max (R1,R2) >= R2 ) by XXREAL_0:25;
consider r being Real such that
A12: ( r > max (R1,R2) & r in dom f ) by A1, LIMFUNC1:46;
A13: ( r > R1 & r > R2 ) by A11, A12, XXREAL_0:2;
then f . r > 0 by A10, A12;
hence contradiction by A9, A12, A13; :: thesis: verum

end;