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 r1 < r & r1 in dom f holds
|.((f . r1) - g).| < g1 by LIMFUNC1:45;
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 r1 < R2 & r1 in dom f holds
g + 1 < f . r1 by A1, LIMFUNC1:48;
set R = min (R1,R2);
A5: ( min (R1,R2) <= R1 & min (R1,R2) <= R2 ) by XXREAL_0:17;
consider r being Real such that
A6: ( r < min (R1,R2) & r in dom f ) by A1, LIMFUNC1:48;
A7: r < R1 by A5, A6, XXREAL_0:2;
r < R2 by A5, A6, XXREAL_0:2;
then A8: 1 < (f . r) - g by A4, A6, 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:49;
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:48;
set R = min (R1,R2);
A11: ( min (R1,R2) <= R1 & min (R1,R2) <= R2 ) by XXREAL_0:17;
consider r being Real such that
A12: ( r < min (R1,R2) & r in dom f ) by A1, LIMFUNC1:48;
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;