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

proof

assume that
A1: seq is increasing and
A2: seq1 is constant ; :: thesis: seq + seq1 is increasing
let n be Nat; :: according to SEQM_3:def 6 :: thesis: (seq + seq1) . n < (seq + seq1) . (n + 1)
consider r1 being Element of REAL such that
A3: for n being Nat holds seq1 . n = r1 by A2;
seq . n < seq . (n + 1) by A1;
then (seq . n) + r1 < (seq . (n + 1)) + r1 by XREAL_1:6;
then (seq . n) + (seq1 . n) < (seq . (n + 1)) + r1 by A3;
then (seq . n) + (seq1 . n) < (seq . (n + 1)) + (seq1 . (n + 1)) by A3;
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 constant implies seq + seq1 is decreasing ) :: thesis: ( ( seq is non-decreasing & seq1 is constant implies seq + seq1 is non-decreasing ) & ( seq is non-increasing & seq1 is constant implies seq + seq1 is non-increasing ) )

proof

assume that
A4: seq is decreasing and
A5: seq1 is constant ; :: thesis: seq + seq1 is decreasing
let n be Nat; :: according to SEQM_3:def 7 :: thesis: (seq + seq1) . n > (seq + seq1) . (n + 1)
consider r1 being Element of REAL such that
A6: for n being Nat holds seq1 . n = r1 by A5;
seq . (n + 1) < seq . n by A4;
then (seq . (n + 1)) + r1 < (seq . n) + r1 by XREAL_1:6;
then (seq . (n + 1)) + (seq1 . (n + 1)) < (seq . n) + r1 by A6;
then (seq . (n + 1)) + (seq1 . (n + 1)) < (seq . n) + (seq1 . n) by A6;
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 constant implies seq + seq1 is non-decreasing ) by Th34; :: thesis: ( seq is non-increasing & seq1 is constant implies seq + seq1 is non-increasing )
assume ( seq is non-increasing & seq1 is constant ) ; :: thesis: seq + seq1 is non-increasing
hence seq + seq1 is non-increasing by Th34; :: thesis: verum