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