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 Element of NAT ; :: according to SEQM_3:def 11 :: thesis: (seq + seq1) . n < (seq + seq1) . (n + 1)
consider r1 being Real such that
A3: for n being Nat holds seq1 . n = r1 by A2, VALUED_0:def 18;
seq . n < seq . (n + 1) by A1, Lm6;
then (seq . n) + r1 < (seq . (n + 1)) + r1 by XREAL_1:8;
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:11;
hence (seq + seq1) . n < (seq + seq1) . (n + 1) by SEQ_1:11; :: 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 Element of NAT ; :: according to SEQM_3:def 12 :: thesis: (seq + seq1) . n > (seq + seq1) . (n + 1)
consider r1 being Real such that
A6: for n being Nat holds seq1 . n = r1 by A5, VALUED_0:def 18;
seq . (n + 1) < seq . n by A4, Lm7;
then (seq . (n + 1)) + r1 < (seq . n) + r1 by XREAL_1:8;
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:11;
hence (seq + seq1) . n > (seq + seq1) . (n + 1) by SEQ_1:11; :: thesis: verum

end;

thus ( seq is non-decreasing & seq1 is constant implies seq + seq1 is non-decreasing ) by Th63; :: 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 Th63; :: thesis: verum