theorem Th21: :: DBLSEQ_3:21

for seq1, seq2 being without-infty ExtREAL_sequence st seq1 is convergent_to_-infty & seq2 is convergent_to_-infty holds
( seq1 + seq2 is convergent_to_-infty & seq1 + seq2 is convergent & lim (seq1 + seq2) = -infty )