let X, Y be set ; :: thesis: for h1, h2 being PartFunc of REAL,REAL holds
( ( h1 | X is increasing & h2 | Y is constant implies (h1 + h2) | (X /\ Y) is increasing ) & ( h1 | X is decreasing & h2 | Y is constant implies (h1 + h2) | (X /\ Y) is decreasing ) )
let h1, h2 be PartFunc of REAL,REAL; :: thesis: ( ( h1 | X is increasing & h2 | Y is constant implies (h1 + h2) | (X /\ Y) is increasing ) & ( h1 | X is decreasing & h2 | Y is constant implies (h1 + h2) | (X /\ Y) is decreasing ) )
thus ( h1 | X is increasing & h2 | Y is constant implies (h1 + h2) | (X /\ Y) is increasing ) :: thesis: ( h1 | X is decreasing & h2 | Y is constant implies (h1 + h2) | (X /\ Y) is decreasing )

proof

assume that
A1: h1 | X is increasing and
A2: h2 | Y is constant ; :: thesis: (h1 + h2) | (X /\ Y) is increasing
consider r being Element of REAL such that
A3: for p being Element of REAL st p in Y /\ (dom h2) holds
h2 . p = r by A2, PARTFUN2:57;

now :: thesis: for r1, r2 being Real st r1 in (X /\ Y) /\ (dom (h1 + h2)) & r2 in (X /\ Y) /\ (dom (h1 + h2)) & r1 < r2 holds
(h1 + h2) . r1 < (h1 + h2) . r2

let r1, r2 be Real; :: thesis: ( r1 in (X /\ Y) /\ (dom (h1 + h2)) & r2 in (X /\ Y) /\ (dom (h1 + h2)) & r1 < r2 implies (h1 + h2) . r1 < (h1 + h2) . r2 )
assume that
A4: r1 in (X /\ Y) /\ (dom (h1 + h2)) and
A5: r2 in (X /\ Y) /\ (dom (h1 + h2)) and
A6: r1 < r2 ; :: thesis: (h1 + h2) . r1 < (h1 + h2) . r2
( r1 in X /\ (dom h1) & r2 in X /\ (dom h1) ) by A4, A5, Th36;
then h1 . r1 < h1 . r2 by A1, A6, Th20;
then A7: (h1 . r1) + r < (h1 . r2) + r by XREAL_1:6;
r1 in Y /\ (dom h2) by A4, Th36;
then A8: (h1 . r1) + (h2 . r1) < (h1 . r2) + r by A3, A7;
A9: r1 in dom (h1 + h2) by A4, XBOOLE_0:def 4;
r2 in Y /\ (dom h2) by A5, Th36;
then (h1 . r1) + (h2 . r1) < (h1 . r2) + (h2 . r2) by A3, A8;
then A10: (h1 + h2) . r1 < (h1 . r2) + (h2 . r2) by A9, VALUED_1:def 1;
r2 in dom (h1 + h2) by A5, XBOOLE_0:def 4;
hence (h1 + h2) . r1 < (h1 + h2) . r2 by A10, VALUED_1:def 1; :: thesis: verum

end;

hence (h1 + h2) | (X /\ Y) is increasing by Th20; :: thesis: verum

end;

assume that
A11: h1 | X is decreasing and
A12: h2 | Y is constant ; :: thesis: (h1 + h2) | (X /\ Y) is decreasing
consider r being Element of REAL such that
A13: for p being Element of REAL st p in Y /\ (dom h2) holds
h2 . p = r by A12, PARTFUN2:57;

now :: thesis: for r1, r2 being Real st r1 in (X /\ Y) /\ (dom (h1 + h2)) & r2 in (X /\ Y) /\ (dom (h1 + h2)) & r1 < r2 holds
(h1 + h2) . r2 < (h1 + h2) . r1

let r1, r2 be Real; :: thesis: ( r1 in (X /\ Y) /\ (dom (h1 + h2)) & r2 in (X /\ Y) /\ (dom (h1 + h2)) & r1 < r2 implies (h1 + h2) . r2 < (h1 + h2) . r1 )
assume that
A14: r1 in (X /\ Y) /\ (dom (h1 + h2)) and
A15: r2 in (X /\ Y) /\ (dom (h1 + h2)) and
A16: r1 < r2 ; :: thesis: (h1 + h2) . r2 < (h1 + h2) . r1
( r1 in X /\ (dom h1) & r2 in X /\ (dom h1) ) by A14, A15, Th36;
then h1 . r2 < h1 . r1 by A11, A16, Th21;
then A17: (h1 . r2) + r < (h1 . r1) + r by XREAL_1:6;
r2 in Y /\ (dom h2) by A15, Th36;
then A18: (h1 . r2) + (h2 . r2) < (h1 . r1) + r by A13, A17;
A19: r2 in dom (h1 + h2) by A15, XBOOLE_0:def 4;
r1 in Y /\ (dom h2) by A14, Th36;
then (h1 . r2) + (h2 . r2) < (h1 . r1) + (h2 . r1) by A13, A18;
then A20: (h1 + h2) . r2 < (h1 . r1) + (h2 . r1) by A19, VALUED_1:def 1;
r1 in dom (h1 + h2) by A14, XBOOLE_0:def 4;
hence (h1 + h2) . r2 < (h1 + h2) . r1 by A20, VALUED_1:def 1; :: thesis: verum

end;

hence (h1 + h2) | (X /\ Y) is decreasing by Th21; :: thesis: verum