theorem Th22: :: DBLSEQ_3:22

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