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: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 r1 > R2 & r1 in dom f holds
g - 1 > f . r1 by A1, LIMFUNC1:47;
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:47;
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:19;
(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, XREAL_1:24; :: 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
0 < f . r1 by LIMFUNC1:46;
consider R2 being Real such that
A10: for r1 being Real st r1 > R2 & r1 in dom f holds
f . r1 < 0 by A1, LIMFUNC1:47;
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:47;
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;