let n be Element of NAT ; :: thesis: for seq1, seq2 being Real_Sequence st seq1 is bounded_below & seq2 is bounded_below holds
(inferior_realsequence (seq1 + seq2)) . n >= ((inferior_realsequence seq1) . n) + ((inferior_realsequence seq2) . n)
let seq1, seq2 be Real_Sequence; :: thesis: ( seq1 is bounded_below & seq2 is bounded_below implies (inferior_realsequence (seq1 + seq2)) . n >= ((inferior_realsequence seq1) . n) + ((inferior_realsequence seq2) . n) )
assume ( seq1 is bounded_below & seq2 is bounded_below ) ; :: thesis: (inferior_realsequence (seq1 + seq2)) . n >= ((inferior_realsequence seq1) . n) + ((inferior_realsequence seq2) . n)
then ( seq1 ^\ n is bounded_below & seq2 ^\ n is bounded_below ) by Th27;
then inf ((seq1 ^\ n) + (seq2 ^\ n)) >= (inf (seq1 ^\ n)) + (inf (seq2 ^\ n)) by Th15;
then A1: inf ((seq1 + seq2) ^\ n) >= (inf (seq1 ^\ n)) + (inf (seq2 ^\ n)) by SEQM_3:37;
( (inferior_realsequence seq1) . n = inf (seq1 ^\ n) & (inferior_realsequence seq2) . n = inf (seq2 ^\ n) ) by Th38;
hence (inferior_realsequence (seq1 + seq2)) . n >= ((inferior_realsequence seq1) . n) + ((inferior_realsequence seq2) . n) by A1, Th38; :: thesis: verum