let seq be convergent ExtREAL_sequence; :: thesis:

P0: now :: thesis:

assume seq is convergent_to_finite_number ; :: thesis:
then consider g being Real such that
A1: ( lim seq = g & ( for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.((seq . m) - (lim seq)).| < p ) ) by MESFUNC9:7;
reconsider G = - g as R_eal by XXREAL_0:def 1;

A5: now :: thesis:

let p be Real; :: thesis:
assume 0 < p ; :: thesis:
then consider n being Nat such that
A2: for m being Nat st n <= m holds
|.((seq . m) - (lim seq)).| < p by A1;
take n = n; :: thesis:

hereby :: thesis:

let m be Nat; :: thesis:
assume n <= m ; :: thesis:
then A3: |.((seq . m) - g).| < p by A1, A2;
m in NAT by ORDINAL1:def 12;
then m in dom (- seq) by FUNCT_2:def 1;
then - (((- seq) . m) - G) = - ((- (seq . m)) - G) by MESFUNC1:def 7
.= - (- ((seq . m) - g)) by XXREAL_3:26
.= (seq . m) - g ;
hence |.(((- seq) . m) - G).| < p by A3, EXTREAL1:29; :: thesis:

end;

end;

hence A4: - seq is convergent_to_finite_number by MESFUNC5:def 8; :: thesis:
hence - seq is convergent ; :: thesis:
lim (- seq) = - g by A4, A5, MESFUNC5:def 12;
hence lim (- seq) = - (lim seq) by A1, XXREAL_3:def 3; :: thesis:

end;

thus ( seq is convergent_to_finite_number implies - seq is convergent_to_finite_number ) by P0; :: thesis:

P1: now :: thesis:

assume A6: seq is convergent_to_+infty ; :: thesis:

A10: now :: thesis:

let g be Real; :: thesis:
assume A7: g < 0 ; :: thesis:
reconsider p = - g as ExtReal ;
consider n being Nat such that
A8: for m being Nat st n <= m holds
p <= seq . m by A6, A7, MESFUNC5:def 9;
take n = n; :: thesis:

hereby :: thesis:

let m be Nat; :: thesis:
assume n <= m ; :: thesis:
then - p >= - (seq . m) by A8, XXREAL_3:38;
then A9: - (- g) >= - (seq . m) by XXREAL_3:def 3;
m in NAT by ORDINAL1:def 12;
then m in dom (- seq) by FUNCT_2:def 1;
hence (- seq) . m <= g by A9, MESFUNC1:def 7; :: thesis:

end;

end;

hence - seq is convergent_to_-infty by MESFUNC5:def 10; :: thesis:
hence - seq is convergent ; :: thesis:
( lim (- seq) = -infty & lim seq = +infty ) by A6, A10, MESFUNC9:7, MESFUNC5:def 10;
hence lim (- seq) = - (lim seq) by XXREAL_3:6; :: thesis:

end;

thus ( seq is convergent_to_+infty implies - seq is convergent_to_-infty ) by P1; :: thesis:

P2: now :: thesis:

assume A11: seq is convergent_to_-infty ; :: thesis:

A15: now :: thesis:

let g be Real; :: thesis:
assume A12: g > 0 ; :: thesis:
reconsider p = - g as ExtReal ;
consider n being Nat such that
A13: for m being Nat st n <= m holds
seq . m <= p by A11, A12, MESFUNC5:def 10;
take n = n; :: thesis:

hereby :: thesis:

let m be Nat; :: thesis:
assume n <= m ; :: thesis:
then - (seq . m) >= - p by A13, XXREAL_3:38;
then A14: - (seq . m) >= - (- g) by XXREAL_3:def 3;
m in NAT by ORDINAL1:def 12;
then m in dom (- seq) by FUNCT_2:def 1;
hence (- seq) . m >= g by A14, MESFUNC1:def 7; :: thesis:

end;

end;

hence - seq is convergent_to_+infty by MESFUNC5:def 9; :: thesis:
hence - seq is convergent ; :: thesis:
( lim (- seq) = +infty & lim seq = -infty ) by A11, A15, MESFUNC9:7, MESFUNC5:def 9;
hence lim (- seq) = - (lim seq) by XXREAL_3:5; :: thesis:

end;

thus ( seq is convergent_to_-infty implies - seq is convergent_to_+infty ) by P2; :: thesis:
thus ( - seq is convergent & lim (- seq) = - (lim seq) ) by P0, P1, P2, MESFUNC5:def 11; :: thesis: