theorem Th23: :: DBLSEQ_3:23

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