let seq, seq1 be Real_Sequence; :: thesis: ( seq is divergent_to-infty & seq1 is convergent implies seq + seq1 is divergent_to-infty )
assume that
A1: seq is divergent_to-infty and
A2: seq1 is convergent ; :: thesis: seq + seq1 is divergent_to-infty
seq1 is bounded by A2;
hence seq + seq1 is divergent_to-infty by A1, Th39; :: thesis: verum