theorem Th8: :: LIMFUNC1:8

for seq1, seq2 being Real_Sequence st seq1 is divergent_to+infty & seq2 is divergent_to+infty holds
seq1 + seq2 is divergent_to+infty