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
R_EAL 1 <= seq . m by Def9;
consider n2 being Nat such that
A3: for m being Nat st n2 <= m holds
seq . m <= R_EAL (- 1) by A1, Def10;
reconsider n1 = n1, n2 = n2 as Element of NAT by ORDINAL1:def 13;
set m = max n1,n2;
( max n1,n2 >= n1 & max n1,n2 >= n2 ) by XXREAL_0:25;
then ( seq . (max n1,n2) <= R_EAL (- 1) & R_EAL 1 <= seq . (max n1,n2) ) by A2, A3;
hence contradiction ; :: 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;
reconsider g1 = - g as Real by XREAL_0:def 1;

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

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

then A6: g1 < - 0 by XREAL_1:26;
consider n1 being Nat such that
A7: for m being Nat st n1 <= m holds
|.((seq . m) - (R_EAL g)).| < R_EAL g by A4, A5;

A8: now

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

end;

consider n2 being Nat such that
A9: for m being Nat st n2 <= m holds
seq . m <= R_EAL g1 by A1, A6, Def10;
reconsider n1 = n1, n2 = n2 as Element of NAT by ORDINAL1:def 13;
set m = max n1,n2;
( n1 <= max n1,n2 & n2 <= max n1,n2 ) by XXREAL_0:25;
then ( seq . (max n1,n2) <= R_EAL g1 & 0 < seq . (max n1,n2) ) by A8, A9;
hence contradiction by A6; :: thesis: verum

end;

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

consider n1 being Nat such that
A11: for m being Nat st n1 <= m holds
|.((seq . m) - (R_EAL g)).| < R_EAL 1 by A4;
consider n2 being Nat such that
A12: for m being Nat st n2 <= m holds
seq . m <= R_EAL (- 1) by A1, Def10;
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 A11, XXREAL_0:25;
then - (R_EAL 1) < (seq . (max n1,n2)) - (R_EAL g) by EXTREAL2:58;
then (- (R_EAL 1)) + (R_EAL g) < seq . (max n1,n2) by EXTREAL2:28;
then - (R_EAL 1) < seq . (max n1,n2) by A10, SUPINF_2:18;
then R_EAL (- 1) < seq . (max n1,n2) by Th7;
hence contradiction by A12, XXREAL_0:25; :: thesis: verum

end;

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

then g1 > 0 by XREAL_1:60;
then consider n1 being Nat such that
A14: for m being Nat st n1 <= m holds
|.((seq . m) - (R_EAL g)).| < R_EAL g1 by A4;

A15: now

let m be Element of NAT ; :: thesis: ( n1 <= m implies R_EAL (2 * g) < seq . m )
assume n1 <= m ; :: thesis: R_EAL (2 * g) < seq . m
then |.((seq . m) - (R_EAL g)).| < R_EAL g1 by A14;
then - (R_EAL g1) < (seq . m) - (R_EAL g) by EXTREAL2:58;
then (- (R_EAL g1)) + (R_EAL g) < seq . m by EXTREAL2:28;
then (R_EAL (- g1)) + (R_EAL g) < seq . m by Th7;
then R_EAL ((- g1) + g) < seq . m by Th7;
hence R_EAL (2 * g) < seq . m ; :: thesis: verum

end;

2 * g < 0 by A13, XREAL_1:134;
then consider n2 being Nat such that
A16: for m being Nat st n2 <= m holds
seq . m <= R_EAL (2 * g) by A1, Def10;
reconsider n1 = n1, n2 = n2 as Element of NAT by ORDINAL1:def 13;
set m = max n1,n2;
( n1 <= max n1,n2 & n2 <= max n1,n2 ) by XXREAL_0:25;
then ( seq . (max n1,n2) <= R_EAL (2 * g) & R_EAL (2 * g) < seq . (max n1,n2) ) by A15, A16;
hence contradiction ; :: thesis: verum

end;

end;