let seq be Real_Sequence; :: thesis: ( seq is divergent_to+infty implies ( not seq is divergent_to-infty & not seq is convergent ) )
assume A1: seq is divergent_to+infty ; :: thesis: ( not seq is divergent_to-infty & not seq is convergent )

hereby :: thesis: not seq is convergent

assume seq is divergent_to-infty ; :: thesis: contradiction
then consider n1 being Nat such that
A2: for m being Nat st n1 <= m holds
seq . m < 0 by LIMFUNC1:def 5;
consider n2 being Nat such that
A3: for m being Nat st n2 <= m holds
seq . m > 0 by A1, LIMFUNC1:def 4;
reconsider m = max (n1,n2) as Element of NAT by ORDINAL1:def 12;
( seq . m < 0 & seq . m > 0 ) by A2, A3, XXREAL_0:25;
hence contradiction ; :: thesis: verum

end;

assume seq is convergent ; :: thesis: contradiction
then consider g being Real such that
A4: for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.((seq . m) - g).| < p by SEQ_2:def 6;

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

suppose g > 0 ; :: thesis: contradiction

then consider n1 being Nat such that
A5: for m being Nat st n1 <= m holds
|.((seq . m) - g).| < g by A4;

A6: now :: thesis: for m being Nat st n1 <= m holds
seq . m < 2 * g

let m be Nat; :: thesis: ( n1 <= m implies seq . m < 2 * g )
assume n1 <= m ; :: thesis: seq . m < 2 * g
then A7: |.((seq . m) - g).| < g by A5;
(seq . m) - g <= |.((seq . m) - g).| by ABSVALUE:4;
then (seq . m) - g < g by A7, XXREAL_0:2;
then seq . m < g + g by XREAL_1:19;
hence seq . m < 2 * g ; :: thesis: verum

end;

consider n2 being Nat such that
A8: for m being Nat st n2 <= m holds
2 * g < seq . m by A1, LIMFUNC1:def 4;
reconsider n1 = n1, n2 = n2 as Element of NAT by ORDINAL1:def 12;
reconsider m = max (n1,n2) as Element of NAT ;
seq . m < 2 * g by A6, XXREAL_0:25;
hence contradiction by A8, XXREAL_0:25; :: thesis: verum

end;

suppose g < 0 ; :: thesis: contradiction

then consider n1 being Nat such that
A9: for m being Nat st n1 <= m holds
|.((seq . m) - g).| < - g by A4, XREAL_1:58;

A10: now :: thesis: for m being Element of NAT st n1 <= m holds
seq . m < 0

let m be Element of NAT ; :: thesis: ( n1 <= m implies seq . m < 0 )
assume n1 <= m ; :: thesis: seq . m < 0
then A11: |.((seq . m) - g).| < - g by A9;
(seq . m) - g <= |.((seq . m) - g).| by ABSVALUE:4;
then (seq . m) - g < - g by A11, XXREAL_0:2;
then seq . m < g - g by XREAL_1:19;
hence seq . m < 0 ; :: thesis: verum

end;

consider n2 being Nat such that
A12: for m being Nat st n2 <= m holds
0 < seq . m by A1, LIMFUNC1:def 4;
reconsider n1 = n1, n2 = n2 as Element of NAT by ORDINAL1:def 12;
reconsider m = max (n1,n2) as Element of NAT ;
seq . m < 0 by A10, XXREAL_0:25;
hence contradiction by A12, XXREAL_0:25; :: thesis: verum

end;

suppose A13: g = 0 ; :: thesis: contradiction

consider n1 being Nat such that
A14: for m being Nat st n1 <= m holds
|.((seq . m) - g).| < 1 by A4;
consider n2 being Nat such that
A15: for m being Nat st n2 <= m holds
1 < seq . m by A1, LIMFUNC1:def 4;
reconsider n1 = n1, n2 = n2 as Element of NAT by ORDINAL1:def 12;
reconsider m = max (n1,n2) as Element of NAT ;
A16: |.((seq . m) - g).| < 1 by A14, XXREAL_0:25;
(seq . m) - g <= |.((seq . m) - g).| by ABSVALUE:4;
then (seq . m) - g < 1 by A16, XXREAL_0:2;
hence contradiction by A13, A15, XXREAL_0:25; :: thesis: verum

end;

end;