let seq1, seq2 be without-infty ExtREAL_sequence; :: thesis: ( seq1 is convergent_to_-infty & seq2 is convergent_to_finite_number implies ( seq1 + seq2 is convergent_to_-infty & seq1 + seq2 is convergent & lim (seq1 + seq2) = -infty ) )
assume A1: ( seq1 is convergent_to_-infty & seq2 is convergent_to_finite_number ) ; :: thesis: ( seq1 + seq2 is convergent_to_-infty & seq1 + seq2 is convergent & lim (seq1 + seq2) = -infty )
then consider S2 being Real such that
A2: for g being Real st 0 < g holds
ex n being Nat st
for m being Nat st n <= m holds
|.((seq2 . m) - S2).| < g by MESFUNC5:def 8;

now :: thesis: for g being Real st g < 0 holds
ex n being Nat st
for m being Nat st n <= m holds
(seq1 + seq2) . m <= g

let g be Real; :: thesis: ( g < 0 implies ex n being Nat st
for m being Nat st n <= m holds
(seq1 + seq2) . m <= g )
assume A3: g < 0 ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
(seq1 + seq2) . m <= g
set G = min ((- 1),((2 * g) - S2));
A4: ( min ((- 1),((2 * g) - S2)) <= - 1 & min ((- 1),((2 * g) - S2)) <= (2 * g) - S2 ) by XXREAL_0:17;
then consider n1 being Nat such that
A5: for m being Nat st n1 <= m holds
seq1 . m <= min ((- 1),((2 * g) - S2)) by A1, MESFUNC5:def 10;
consider n2 being Nat such that
A6: for m being Nat st n2 <= m holds
|.((seq2 . m) - S2).| < - g by A2, A3;
reconsider N1 = n1, N2 = n2 as Element of NAT by ORDINAL1:def 12;
reconsider n = max (N1,N2) as Nat ;
A7: ( n1 <= n & n2 <= n ) by XXREAL_0:25;

now :: thesis: for m being Nat st n <= m holds
(seq1 + seq2) . m <= g

let m be Nat; :: thesis: ( n <= m implies (seq1 + seq2) . m <= g )
assume n <= m ; :: thesis: (seq1 + seq2) . m <= g
then ( n1 <= m & n2 <= m ) by A7, XXREAL_0:2;
then A8: ( seq1 . m <= min ((- 1),((2 * g) - S2)) & |.((seq2 . m) - S2).| < - g ) by A5, A6;
reconsider g1 = g as R_eal by XXREAL_0:def 1;
B1: - g1 = - g by XXREAL_3:def 3;
then (seq2 . m) - S2 < - g1 by A8, EXTREAL1:21;
then seq2 . m < (- g1) + S2 by XXREAL_3:54;
then A9: (seq1 . m) + (seq2 . m) <= (min ((- 1),((2 * g) - S2))) + ((- g1) + S2) by A8, XXREAL_3:36;
(- g1) + S2 = (- g) + S2 by B1, XXREAL_3:def 2;
then ((2 * g) - S2) + ((- g1) + S2) = ((2 * g) - S2) + ((- g) + S2) by XXREAL_3:def 2;
then (min ((- 1),((2 * g) - S2))) + ((- g1) + S2) <= g by A4, XXREAL_3:36;
then A10: (seq1 . m) + (seq2 . m) <= g by A9, XXREAL_0:2;
m is Element of NAT by ORDINAL1:def 12;
hence (seq1 + seq2) . m <= g by A10, Th7; :: thesis: verum

end;

hence ex n being Nat st
for m being Nat st n <= m holds
(seq1 + seq2) . m <= g ; :: thesis: verum

end;

hence A11: seq1 + seq2 is convergent_to_-infty by MESFUNC5:def 10; :: thesis: ( seq1 + seq2 is convergent & lim (seq1 + seq2) = -infty )
hence seq1 + seq2 is convergent ; :: thesis: lim (seq1 + seq2) = -infty
thus lim (seq1 + seq2) = -infty by A11, MESFUNC5:def 12; :: thesis: verum