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, Th36; :: thesis: verum