let seq be ExtREAL_sequence; :: thesis: ( seq is convergent_to_+infty implies ( not seq is convergent_to_-infty & not seq is convergent_to_finite_number ) )
assume A1: seq is convergent_to_+infty ; :: thesis: ( not seq is convergent_to_-infty & not seq is convergent_to_finite_number )

hereby :: thesis: not seq is convergent_to_finite_number

assume seq is convergent_to_-infty ; :: thesis: contradiction
then consider n1 being Nat such that
A2: for m being Nat st n1 <= m holds
seq . m <= R_EAL (- 1) by Def10;
consider n2 being Nat such that
A3: for m being Nat st n2 <= m holds
R_EAL 1 <= seq . m by A1, Def9;
reconsider n1 = n1, n2 = n2 as Element of NAT by ORDINAL1:def 13;
set m = max (n1,n2);
seq . (max (n1,n2)) <= R_EAL (- 1) by A2, XXREAL_0:25;
hence contradiction by A3, XXREAL_0:25; :: thesis: verum

end;

assume seq is convergent_to_finite_number ; :: thesis: contradiction
then consider g being real number such that
A4: for p being real number st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.((seq . m) - (R_EAL g)).| < p by Def8;

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

suppose A5: g > 0 ; :: thesis: contradiction

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

A7: now

let m be Nat; :: thesis: ( n1 <= m implies seq . m < R_EAL (2 * g) )
assume n1 <= m ; :: thesis: seq . m < R_EAL (2 * g)
then |.((seq . m) - (R_EAL g)).| < R_EAL g by A6;
then (seq . m) - (R_EAL g) < R_EAL g by EXTREAL2:58;
then seq . m < R_EAL (g + g) by XXREAL_3:65;
hence seq . m < R_EAL (2 * g) ; :: thesis: verum

end;

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

end;

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

consider n1 being Nat such that
A10: for m being Nat st n1 <= m holds
|.((seq . m) - (R_EAL g)).| < R_EAL 1 by A4;
consider n2 being Nat such that
A11: for m being Nat st n2 <= m holds
R_EAL 1 <= seq . m by A1, Def9;
reconsider n1 = n1, n2 = n2 as Element of NAT by ORDINAL1:def 13;
set m = max (n1,n2);
|.((seq . (max (n1,n2))) - (R_EAL g)).| < R_EAL 1 by A10, XXREAL_0:25;
then (seq . (max (n1,n2))) - (R_EAL g) < R_EAL 1 by EXTREAL2:58;
then seq . (max (n1,n2)) < (R_EAL 1) + (R_EAL g) by XXREAL_3:65;
then seq . (max (n1,n2)) < R_EAL 1 by A9, XXREAL_3:4;
hence contradiction by A11, XXREAL_0:25; :: thesis: verum

end;

suppose A12: g < 0 ; :: thesis: contradiction

set g1 = - g;
consider n1 being Nat such that
A13: for m being Nat st n1 <= m holds
|.((seq . m) - (R_EAL g)).| < R_EAL (- g) by A4, A12;

A14: now

let m be Element of NAT ; :: thesis: ( n1 <= m implies seq . m < 0 )
assume n1 <= m ; :: thesis: seq . m < 0
then |.((seq . m) - (R_EAL g)).| < R_EAL (- g) by A13;
then (seq . m) - (R_EAL g) < R_EAL (- g) by EXTREAL2:58;
then seq . m < (- g) + g by XXREAL_3:65;
hence seq . m < 0 ; :: thesis: verum

end;

consider n2 being Nat such that
A15: for m being Nat st n2 <= m holds
1 <= seq . m by A1, Def9;
reconsider n1 = n1, n2 = n2 as Element of NAT by ORDINAL1:def 13;
set m = max (n1,n2);
seq . (max (n1,n2)) < 0 by A14, XXREAL_0:25;
hence contradiction by A15, XXREAL_0:25; :: thesis: verum

end;

end;