let n be Element of 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 Th26;
then sup ((seq1 ^\ n) + (seq2 ^\ n)) <= (sup (seq1 ^\ n)) + (sup (seq2 ^\ n)) by Th16;
then A1: sup ((seq1 + seq2) ^\ n) <= (sup (seq1 ^\ n)) + (sup (seq2 ^\ n)) by SEQM_3:37;
( (superior_realsequence seq1) . n = sup (seq1 ^\ n) & (superior_realsequence seq2) . n = sup (seq2 ^\ n) ) by Th39;
hence (superior_realsequence (seq1 + seq2)) . n <= ((superior_realsequence seq1) . n) + ((superior_realsequence seq2) . n) by A1, Th39; :: thesis: verum