let seq1, seq2 be Real_Sequence; :: thesis: ( seq1 is bounded_below & seq2 is bounded_below implies inf (seq1 + seq2) >= (inf seq1) + (inf seq2) )
assume that
A1: seq1 is bounded_below and
A2: seq2 is bounded_below ; :: thesis: inf (seq1 + seq2) >= (inf seq1) + (inf seq2)
for n being Element of NAT holds (seq1 + seq2) . n >= (inf seq1) + (inf seq2)

proof

let n be Element of NAT ; :: thesis: (seq1 + seq2) . n >= (inf seq1) + (inf seq2)
A3: seq2 . n >= inf seq2 by A2, Th8;
( (seq1 + seq2) . n = (seq1 . n) + (seq2 . n) & seq1 . n >= inf seq1 ) by A1, Th8, SEQ_1:11;
hence (seq1 + seq2) . n >= (inf seq1) + (inf seq2) by A3, XREAL_1:9; :: thesis: verum

end;

hence inf (seq1 + seq2) >= (inf seq1) + (inf seq2) by Th10; :: thesis: verum