let seq1, seq2 be Real_Sequence; :: thesis: ( seq1 is bounded_above & seq2 is bounded_above implies upper_bound (seq1 + seq2) <= (upper_bound seq1) + (upper_bound seq2) )
assume that
A1: seq1 is bounded_above and
A2: seq2 is bounded_above ; :: thesis: upper_bound (seq1 + seq2) <= (upper_bound seq1) + (upper_bound seq2)
for n being Nat holds (seq1 + seq2) . n <= (upper_bound seq1) + (upper_bound seq2)

proof

let n be Nat; :: thesis: (seq1 + seq2) . n <= (upper_bound seq1) + (upper_bound seq2)
A3: seq2 . n <= upper_bound seq2 by A2, Th7;
( (seq1 + seq2) . n = (seq1 . n) + (seq2 . n) & seq1 . n <= upper_bound seq1 ) by A1, Th7, SEQ_1:7;
hence (seq1 + seq2) . n <= (upper_bound seq1) + (upper_bound seq2) by A3, XREAL_1:7; :: thesis: verum

end;

hence upper_bound (seq1 + seq2) <= (upper_bound seq1) + (upper_bound seq2) by Th9; :: thesis: verum