let seq1, seq2 be Real_Sequence; :: thesis: ( seq1 is divergent_to-infty & seq2 is bounded_above implies seq1 + seq2 is divergent_to-infty )
assume A1: ( seq1 is divergent_to-infty & seq2 is bounded_above ) ; :: thesis: seq1 + seq2 is divergent_to-infty
then consider M being real number such that
A2: for n being Element of NAT holds seq2 . n < M by SEQ_2:def 3;
let r be Real; :: according to LIMFUNC1:def 5 :: thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
(seq1 + seq2) . m < r
consider n being Element of NAT such that
A3: for m being Element of NAT st n <= m holds
seq1 . m < r - M by A1, Def5;
take n ; :: thesis: for m being Element of NAT st n <= m holds
(seq1 + seq2) . m < r
let m be Element of NAT ; :: thesis: ( n <= m implies (seq1 + seq2) . m < r )
assume n <= m ; :: thesis: (seq1 + seq2) . m < r
then seq1 . m < r - M by A3;
then (seq1 . m) + (seq2 . m) < (r - M) + M by A2, XREAL_1:10;
hence (seq1 + seq2) . m < r by SEQ_1:11; :: thesis: verum