let seq be convergent ExtREAL_sequence; :: thesis: ( ( seq is convergent_to_finite_number implies - seq is convergent_to_finite_number ) & ( seq is convergent_to_+infty implies - seq is convergent_to_-infty ) & ( seq is convergent_to_-infty implies - seq is convergent_to_+infty ) & - seq is convergent & lim (- seq) = - (lim seq) )

P0: now :: thesis: ( seq is convergent_to_finite_number implies ( - seq is convergent_to_finite_number & - seq is convergent & lim (- seq) = - (lim seq) ) )

assume seq is convergent_to_finite_number ; :: thesis: ( - seq is convergent_to_finite_number & - seq is convergent & lim (- seq) = - (lim seq) )
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: 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

let p be Real; :: thesis: ( 0 < p implies ex n being Nat st
for m being Nat st n <= m holds
|.(((- seq) . m) - G).| < p )
assume 0 < p ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
|.(((- seq) . m) - G).| < p
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: for m being Nat st n <= m holds
|.(((- seq) . m) - G).| < p

hereby :: thesis: verum

let m be Nat; :: thesis: ( n <= m implies |.(((- seq) . m) - G).| < p )
assume n <= m ; :: thesis: |.(((- seq) . m) - G).| < p
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: verum

end;

end;

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

end;

thus ( seq is convergent_to_finite_number implies - seq is convergent_to_finite_number ) by P0; :: thesis: ( ( seq is convergent_to_+infty implies - seq is convergent_to_-infty ) & ( seq is convergent_to_-infty implies - seq is convergent_to_+infty ) & - seq is convergent & lim (- seq) = - (lim seq) )

P1: now :: thesis: ( seq is convergent_to_+infty implies ( - seq is convergent_to_-infty & - seq is convergent & lim (- seq) = - (lim seq) ) )

assume A6: seq is convergent_to_+infty ; :: thesis: ( - seq is convergent_to_-infty & - seq is convergent & lim (- seq) = - (lim seq) )

A10: now :: thesis: for g being Real st g < 0 holds
ex n being Nat st
for m being Nat st n <= m holds
(- seq) . m <= g

let g be Real; :: thesis: ( g < 0 implies ex n being Nat st
for m being Nat st n <= m holds
(- seq) . m <= g )
assume A7: g < 0 ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
(- seq) . m <= g
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: for m being Nat st n <= m holds
(- seq) . m <= g

hereby :: thesis: verum

let m be Nat; :: thesis: ( n <= m implies (- seq) . m <= g )
assume n <= m ; :: thesis: (- seq) . m <= g
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: verum

end;

end;

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

end;

thus ( seq is convergent_to_+infty implies - seq is convergent_to_-infty ) by P1; :: thesis: ( ( seq is convergent_to_-infty implies - seq is convergent_to_+infty ) & - seq is convergent & lim (- seq) = - (lim seq) )

P2: now :: thesis: ( seq is convergent_to_-infty implies ( - seq is convergent_to_+infty & - seq is convergent & lim (- seq) = - (lim seq) ) )

assume A11: seq is convergent_to_-infty ; :: thesis: ( - seq is convergent_to_+infty & - seq is convergent & lim (- seq) = - (lim seq) )

A15: now :: thesis: for g being Real st g > 0 holds
ex n being Nat st
for m being Nat st n <= m holds
(- seq) . m >= g

let g be Real; :: thesis: ( g > 0 implies ex n being Nat st
for m being Nat st n <= m holds
(- seq) . m >= g )
assume A12: g > 0 ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
(- seq) . m >= g
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: for m being Nat st n <= m holds
(- seq) . m >= g

hereby :: thesis: verum

let m be Nat; :: thesis: ( n <= m implies (- seq) . m >= g )
assume n <= m ; :: thesis: (- seq) . m >= g
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: verum

end;

end;

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

end;

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