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 Nat; :: according to SEQM_3:def 6 :: thesis: (seq + seq1) . n < (seq + seq1) . (n + 1)
( seq . n < seq . (n + 1) & seq1 . n < seq1 . (n + 1) ) by A1;
then (seq . n) + (seq1 . n) < (seq . (n + 1)) + (seq1 . (n + 1)) by XREAL_1:8;
then (seq + seq1) . n < (seq . (n + 1)) + (seq1 . (n + 1)) by SEQ_1:7;
hence (seq + seq1) . n < (seq + seq1) . (n + 1) by SEQ_1:7; :: 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 Nat; :: according to SEQM_3:def 7 :: thesis: (seq + seq1) . n > (seq + seq1) . (n + 1)
( seq . (n + 1) < seq . n & seq1 . (n + 1) < seq1 . n ) by A2;
then (seq . (n + 1)) + (seq1 . (n + 1)) < (seq . n) + (seq1 . n) by XREAL_1:8;
then (seq + seq1) . (n + 1) < (seq . n) + (seq1 . n) by SEQ_1:7;
hence (seq + seq1) . n > (seq + seq1) . (n + 1) by SEQ_1:7; :: 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 Nat; :: according to SEQM_3:def 8 :: thesis: (seq + seq1) . n <= (seq + seq1) . (n + 1)
( seq . n <= seq . (n + 1) & seq1 . n <= seq1 . (n + 1) ) by A3;
then (seq . n) + (seq1 . n) <= (seq . (n + 1)) + (seq1 . (n + 1)) by XREAL_1:7;
then (seq + seq1) . n <= (seq . (n + 1)) + (seq1 . (n + 1)) by SEQ_1:7;
hence (seq + seq1) . n <= (seq + seq1) . (n + 1) by SEQ_1:7; :: thesis: verum

end;

assume A4: ( seq is non-increasing & seq1 is non-increasing ) ; :: thesis: seq + seq1 is non-increasing
let n be Nat; :: according to SEQM_3:def 9 :: thesis: (seq + seq1) . n >= (seq + seq1) . (n + 1)
( seq . (n + 1) <= seq . n & seq1 . (n + 1) <= seq1 . n ) by A4;
then (seq . (n + 1)) + (seq1 . (n + 1)) <= (seq . n) + (seq1 . n) by XREAL_1:7;
then (seq + seq1) . (n + 1) <= (seq . n) + (seq1 . n) by SEQ_1:7;
hence (seq + seq1) . n >= (seq + seq1) . (n + 1) by SEQ_1:7; :: thesis: verum