let seq1, seq2 be without-infty ExtREAL_sequence; :: thesis: ( seq1 is convergent_to_-infty & seq2 is convergent_to_-infty 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_-infty ) ; :: thesis: ( seq1 + seq2 is convergent_to_-infty & seq1 + seq2 is convergent & lim (seq1 + seq2) = -infty )

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 A2: g < 0 ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
(seq1 + seq2) . m <= g
then consider n1 being Nat such that
A3: for m being Nat st n1 <= m holds
seq1 . m <= g / 2 by A1, MESFUNC5:def 10;
consider n2 being Nat such that
A4: for m being Nat st n2 <= m holds
seq2 . m <= g / 2 by A1, A2, MESFUNC5:def 10;
reconsider N1 = n1, N2 = n2 as Element of NAT by ORDINAL1:def 12;
reconsider n = max (N1,N2) as Nat ;
A5: ( 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 A5, XXREAL_0:2;
then ( seq1 . m <= g / 2 & seq2 . m <= g / 2 ) by A3, A4;
then A6: (seq1 . m) + (seq2 . m) <= (g / 2) + (g / 2) by XXREAL_3:36;
m is Element of NAT by ORDINAL1:def 12;
hence (seq1 + seq2) . m <= g by A6, 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 A7: 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 A7, MESFUNC5:def 12; :: thesis: verum