let seq, seq1 be Real_Sequence; :: thesis: ( seq is bounded_below & seq1 is non-decreasing implies seq + seq1 is bounded_below )
assume that
A1: seq is bounded_below and
A2: seq1 is non-decreasing ; :: thesis: seq + seq1 is bounded_below
consider r1 being real number such that
A3: for n being Element of NAT holds r1 < seq . n by A1, SEQ_2:def 4;
take r = r1 + (seq1 . 0 ); :: according to SEQ_2:def 4 :: thesis: for b₁ being Element of NAT holds not (seq + seq1) . b₁ <= r
let n be Element of NAT ; :: thesis: not (seq + seq1) . n <= r
seq1 . 0 <= seq1 . n by A2, Th21;
then r1 + (seq1 . 0 ) < (seq . n) + (seq1 . n) by A3, XREAL_1:10;
hence r < (seq + seq1) . n by SEQ_1:11; :: thesis: verum