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