let n be Nat; :: thesis: for seq1, seq2 being Real_Sequence st seq1 is bounded_above & seq2 is bounded_above holds
(superior_realsequence (seq1 + seq2)) . n <= ((superior_realsequence seq1) . n) + ((superior_realsequence seq2) . n)
let seq1, seq2 be Real_Sequence; :: thesis: ( seq1 is bounded_above & seq2 is bounded_above implies (superior_realsequence (seq1 + seq2)) . n <= ((superior_realsequence seq1) . n) + ((superior_realsequence seq2) . n) )
assume ( seq1 is bounded_above & seq2 is bounded_above ) ; :: thesis: (superior_realsequence (seq1 + seq2)) . n <= ((superior_realsequence seq1) . n) + ((superior_realsequence seq2) . n)
then ( seq1 ^\ n is bounded_above & seq2 ^\ n is bounded_above ) by SEQM_3:27;
then upper_bound ((seq1 ^\ n) + (seq2 ^\ n)) <= (upper_bound (seq1 ^\ n)) + (upper_bound (seq2 ^\ n)) by Th16;
then A1: upper_bound ((seq1 + seq2) ^\ n) <= (upper_bound (seq1 ^\ n)) + (upper_bound (seq2 ^\ n)) by SEQM_3:15;
( (superior_realsequence seq1) . n = upper_bound (seq1 ^\ n) & (superior_realsequence seq2) . n = upper_bound (seq2 ^\ n) ) by Th37;
hence (superior_realsequence (seq1 + seq2)) . n <= ((superior_realsequence seq1) . n) + ((superior_realsequence seq2) . n) by A1, Th37; :: thesis: verum