theorem :: LIMFUNC1:19

for seq, seq1 being Real_Sequence st seq is divergent_to-infty & seq1 is convergent holds
seq + seq1 is divergent_to-infty by Th12;