let seq, seq1 be Real_Sequence; :: thesis: ( ( seq is increasing & seq1 is increasing implies seq + seq1 is increasing ) & ( seq is decreasing & seq1 is decreasing implies seq + seq1 is decreasing ) & ( seq is non-decreasing & seq1 is non-decreasing implies seq + seq1 is non-decreasing ) & ( seq is non-increasing & seq1 is non-increasing implies seq + seq1 is non-increasing ) )
thus ( seq is increasing & seq1 is increasing implies seq + seq1 is increasing ) :: thesis: ( ( seq is decreasing & seq1 is decreasing implies seq + seq1 is decreasing ) & ( seq is non-decreasing & seq1 is non-decreasing implies seq + seq1 is non-decreasing ) & ( seq is non-increasing & seq1 is non-increasing implies seq + seq1 is non-increasing ) )

proof

assume A1: ( seq is increasing & seq1 is increasing ) ; :: thesis: seq + seq1 is increasing
let n be Element of NAT ; :: according to SEQM_3:def 11 :: thesis: (seq + seq1) . n < (seq + seq1) . (n + 1)
( seq . n < seq . (n + 1) & seq1 . n < seq1 . (n + 1) ) by A1, Lm6;
then (seq . n) + (seq1 . n) < (seq . (n + 1)) + (seq1 . (n + 1)) by XREAL_1:10;
then (seq + seq1) . n < (seq . (n + 1)) + (seq1 . (n + 1)) by SEQ_1:11;
hence (seq + seq1) . n < (seq + seq1) . (n + 1) by SEQ_1:11; :: thesis: verum

end;

thus ( seq is decreasing & seq1 is decreasing implies seq + seq1 is decreasing ) :: thesis: ( ( seq is non-decreasing & seq1 is non-decreasing implies seq + seq1 is non-decreasing ) & ( seq is non-increasing & seq1 is non-increasing implies seq + seq1 is non-increasing ) )

proof

assume A2: ( seq is decreasing & seq1 is decreasing ) ; :: thesis: seq + seq1 is decreasing
let n be Element of NAT ; :: according to SEQM_3:def 12 :: thesis: (seq + seq1) . n > (seq + seq1) . (n + 1)
( seq . (n + 1) < seq . n & seq1 . (n + 1) < seq1 . n ) by A2, Lm7;
then (seq . (n + 1)) + (seq1 . (n + 1)) < (seq . n) + (seq1 . n) by XREAL_1:10;
then (seq + seq1) . (n + 1) < (seq . n) + (seq1 . n) by SEQ_1:11;
hence (seq + seq1) . n > (seq + seq1) . (n + 1) by SEQ_1:11; :: thesis: verum

end;

thus ( seq is non-decreasing & seq1 is non-decreasing implies seq + seq1 is non-decreasing ) :: thesis: ( seq is non-increasing & seq1 is non-increasing implies seq + seq1 is non-increasing )

proof

assume A3: ( seq is non-decreasing & seq1 is non-decreasing ) ; :: thesis: seq + seq1 is non-decreasing
let n be Element of NAT ; :: according to SEQM_3:def 13 :: thesis: (seq + seq1) . n <= (seq + seq1) . (n + 1)
( seq . n <= seq . (n + 1) & seq1 . n <= seq1 . (n + 1) ) by A3, Lm8;
then (seq . n) + (seq1 . n) <= (seq . (n + 1)) + (seq1 . (n + 1)) by XREAL_1:9;
then (seq + seq1) . n <= (seq . (n + 1)) + (seq1 . (n + 1)) by SEQ_1:11;
hence (seq + seq1) . n <= (seq + seq1) . (n + 1) by SEQ_1:11; :: thesis: verum

end;

assume A4: ( seq is non-increasing & seq1 is non-increasing ) ; :: thesis: seq + seq1 is non-increasing
let n be Element of NAT ; :: according to SEQM_3:def 14 :: thesis: (seq + seq1) . n >= (seq + seq1) . (n + 1)
( seq . (n + 1) <= seq . n & seq1 . (n + 1) <= seq1 . n ) by A4, Lm9;
then (seq . (n + 1)) + (seq1 . (n + 1)) <= (seq . n) + (seq1 . n) by XREAL_1:9;
then (seq + seq1) . (n + 1) <= (seq . n) + (seq1 . n) by SEQ_1:11;
hence (seq + seq1) . n >= (seq + seq1) . (n + 1) by SEQ_1:11; :: thesis: verum