theorem Th18: :: DBLSEQ_3:18

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 )