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

proof

assume that
A1: h1 | X is increasing and
A2: h2 | Y is increasing ; :: thesis: (h1 + h2) | (X /\ Y) is increasing

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
A3: r1 in (X /\ Y) /\ (dom (h1 + h2)) and
A4: r2 in (X /\ Y) /\ (dom (h1 + h2)) and
A5: r1 < r2 ; :: thesis: (h1 + h2) . r1 < (h1 + h2) . r2
( r1 in Y /\ (dom h2) & r2 in Y /\ (dom h2) ) by A3, A4, Th36;
then A6: h2 . r1 < h2 . r2 by A2, A5, Th20;
A7: r1 in dom (h1 + h2) by A3, XBOOLE_0:def 4;
( r1 in X /\ (dom h1) & r2 in X /\ (dom h1) ) by A3, A4, Th36;
then h1 . r1 < h1 . r2 by A1, A5, Th20;
then (h1 . r1) + (h2 . r1) < (h1 . r2) + (h2 . r2) by A6, XREAL_1:8;
then A8: (h1 + h2) . r1 < (h1 . r2) + (h2 . r2) by A7, VALUED_1:def 1;
r2 in dom (h1 + h2) by A4, XBOOLE_0:def 4;
hence (h1 + h2) . r1 < (h1 + h2) . r2 by A8, VALUED_1:def 1; :: thesis: verum

end;

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

end;

thus ( h1 | X is decreasing & h2 | Y is decreasing implies (h1 + h2) | (X /\ Y) is decreasing ) :: thesis: ( ( h1 | X is non-decreasing & h2 | Y is non-decreasing implies (h1 + h2) | (X /\ Y) is non-decreasing ) & ( h1 | X is non-increasing & h2 | Y is non-increasing implies (h1 + h2) | (X /\ Y) is non-increasing ) )

proof

assume that
A9: h1 | X is decreasing and
A10: h2 | Y is decreasing ; :: thesis: (h1 + h2) | (X /\ Y) is decreasing

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
A11: r1 in (X /\ Y) /\ (dom (h1 + h2)) and
A12: r2 in (X /\ Y) /\ (dom (h1 + h2)) and
A13: r1 < r2 ; :: thesis: (h1 + h2) . r2 < (h1 + h2) . r1
( r1 in Y /\ (dom h2) & r2 in Y /\ (dom h2) ) by A11, A12, Th36;
then A14: h2 . r2 < h2 . r1 by A10, A13, Th21;
A15: r2 in dom (h1 + h2) by A12, XBOOLE_0:def 4;
( r1 in X /\ (dom h1) & r2 in X /\ (dom h1) ) by A11, A12, Th36;
then h1 . r2 < h1 . r1 by A9, A13, Th21;
then (h1 . r2) + (h2 . r2) < (h1 . r1) + (h2 . r1) by A14, XREAL_1:8;
then A16: (h1 + h2) . r2 < (h1 . r1) + (h2 . r1) by A15, VALUED_1:def 1;
r1 in dom (h1 + h2) by A11, XBOOLE_0:def 4;
hence (h1 + h2) . r2 < (h1 + h2) . r1 by A16, VALUED_1:def 1; :: thesis: verum

end;

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

end;

thus ( h1 | X is non-decreasing & h2 | Y is non-decreasing implies (h1 + h2) | (X /\ Y) is non-decreasing ) :: thesis: ( h1 | X is non-increasing & h2 | Y is non-increasing implies (h1 + h2) | (X /\ Y) is non-increasing )

proof

assume that
A17: h1 | X is non-decreasing and
A18: h2 | Y is non-decreasing ; :: thesis: (h1 + h2) | (X /\ Y) is non-decreasing

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
A19: r1 in (X /\ Y) /\ (dom (h1 + h2)) and
A20: r2 in (X /\ Y) /\ (dom (h1 + h2)) and
A21: r1 < r2 ; :: thesis: (h1 + h2) . r1 <= (h1 + h2) . r2
( r1 in Y /\ (dom h2) & r2 in Y /\ (dom h2) ) by A19, A20, Th36;
then A22: h2 . r1 <= h2 . r2 by A18, A21, Th22;
A23: r1 in dom (h1 + h2) by A19, XBOOLE_0:def 4;
( r1 in X /\ (dom h1) & r2 in X /\ (dom h1) ) by A19, A20, Th36;
then h1 . r1 <= h1 . r2 by A17, A21, Th22;
then (h1 . r1) + (h2 . r1) <= (h1 . r2) + (h2 . r2) by A22, XREAL_1:7;
then A24: (h1 + h2) . r1 <= (h1 . r2) + (h2 . r2) by A23, VALUED_1:def 1;
r2 in dom (h1 + h2) by A20, XBOOLE_0:def 4;
hence (h1 + h2) . r1 <= (h1 + h2) . r2 by A24, VALUED_1:def 1; :: thesis: verum

end;

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

end;

assume that
A25: h1 | X is non-increasing and
A26: h2 | Y is non-increasing ; :: thesis: (h1 + h2) | (X /\ Y) is non-increasing

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
A27: r1 in (X /\ Y) /\ (dom (h1 + h2)) and
A28: r2 in (X /\ Y) /\ (dom (h1 + h2)) and
A29: r1 < r2 ; :: thesis: (h1 + h2) . r2 <= (h1 + h2) . r1
( r1 in Y /\ (dom h2) & r2 in Y /\ (dom h2) ) by A27, A28, Th36;
then A30: h2 . r2 <= h2 . r1 by A26, A29, Th23;
A31: r2 in dom (h1 + h2) by A28, XBOOLE_0:def 4;
( r1 in X /\ (dom h1) & r2 in X /\ (dom h1) ) by A27, A28, Th36;
then h1 . r2 <= h1 . r1 by A25, A29, Th23;
then (h1 . r2) + (h2 . r2) <= (h1 . r1) + (h2 . r1) by A30, XREAL_1:7;
then A32: (h1 + h2) . r2 <= (h1 . r1) + (h2 . r1) by A31, VALUED_1:def 1;
r1 in dom (h1 + h2) by A27, XBOOLE_0:def 4;
hence (h1 + h2) . r2 <= (h1 + h2) . r1 by A32, VALUED_1:def 1; :: thesis: verum

end;

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