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 A1: ( h1 | X is increasing & h2 | Y is increasing ) ; :: thesis: (h1 + h2) | (X /\ Y) is increasing

now

let r1, r2 be Element of 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 A2: ( r1 in (X /\ Y) /\ (dom (h1 + h2)) & r2 in (X /\ Y) /\ (dom (h1 + h2)) & r1 < r2 ) ; :: thesis: (h1 + h2) . r1 < (h1 + h2) . r2
then A3: ( r1 in X /\ (dom h1) & r1 in Y /\ (dom h2) ) by Th68;
A4: ( r2 in X /\ (dom h1) & r2 in Y /\ (dom h2) ) by A2, Th68;
A5: ( r1 in dom (h1 + h2) & r2 in dom (h1 + h2) & r1 < r2 ) by A2, XBOOLE_0:def 4;
A6: h1 . r1 < h1 . r2 by A1, A2, A3, A4, Def2;
h2 . r1 < h2 . r2 by A1, A2, A3, A4, Def2;
then (h1 . r1) + (h2 . r1) < (h1 . r2) + (h2 . r2) by A6, XREAL_1:10;
then (h1 + h2) . r1 < (h1 . r2) + (h2 . r2) by A5, VALUED_1:def 1;
hence (h1 + h2) . r1 < (h1 + h2) . r2 by A5, VALUED_1:def 1; :: thesis: verum

end;

hence (h1 + h2) | (X /\ Y) is increasing by Def2; :: 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 A7: ( h1 | X is decreasing & h2 | Y is decreasing ) ; :: thesis: (h1 + h2) | (X /\ Y) is decreasing

now

let r1, r2 be Element of 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 A8: ( r1 in (X /\ Y) /\ (dom (h1 + h2)) & r2 in (X /\ Y) /\ (dom (h1 + h2)) & r1 < r2 ) ; :: thesis: (h1 + h2) . r2 < (h1 + h2) . r1
then A9: ( r1 in X /\ (dom h1) & r1 in Y /\ (dom h2) ) by Th68;
A10: ( r2 in X /\ (dom h1) & r2 in Y /\ (dom h2) ) by A8, Th68;
A11: ( r1 in dom (h1 + h2) & r2 in dom (h1 + h2) & r1 < r2 ) by A8, XBOOLE_0:def 4;
A12: h1 . r2 < h1 . r1 by A7, A8, A9, A10, Def3;
h2 . r2 < h2 . r1 by A7, A8, A9, A10, Def3;
then (h1 . r2) + (h2 . r2) < (h1 . r1) + (h2 . r1) by A12, XREAL_1:10;
then (h1 + h2) . r2 < (h1 . r1) + (h2 . r1) by A11, VALUED_1:def 1;
hence (h1 + h2) . r2 < (h1 + h2) . r1 by A11, VALUED_1:def 1; :: thesis: verum

end;

hence (h1 + h2) | (X /\ Y) is decreasing by Def3; :: 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 A13: ( h1 | X is non-decreasing & h2 | Y is non-decreasing ) ; :: thesis: (h1 + h2) | (X /\ Y) is non-decreasing

now

let r1, r2 be Element of 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 A14: ( r1 in (X /\ Y) /\ (dom (h1 + h2)) & r2 in (X /\ Y) /\ (dom (h1 + h2)) & r1 < r2 ) ; :: thesis: (h1 + h2) . r1 <= (h1 + h2) . r2
then A15: ( r1 in X /\ (dom h1) & r1 in Y /\ (dom h2) ) by Th68;
A16: ( r2 in X /\ (dom h1) & r2 in Y /\ (dom h2) ) by A14, Th68;
A17: ( r1 in dom (h1 + h2) & r2 in dom (h1 + h2) & r1 < r2 ) by A14, XBOOLE_0:def 4;
A18: h1 . r1 <= h1 . r2 by A13, A14, A15, A16, Def4;
h2 . r1 <= h2 . r2 by A13, A14, A15, A16, Def4;
then (h1 . r1) + (h2 . r1) <= (h1 . r2) + (h2 . r2) by A18, XREAL_1:9;
then (h1 + h2) . r1 <= (h1 . r2) + (h2 . r2) by A17, VALUED_1:def 1;
hence (h1 + h2) . r1 <= (h1 + h2) . r2 by A17, VALUED_1:def 1; :: thesis: verum

end;

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

end;

assume A19: ( h1 | X is non-increasing & h2 | Y is non-increasing ) ; :: thesis: (h1 + h2) | (X /\ Y) is non-increasing

now

let r1, r2 be Element of 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 A20: ( r1 in (X /\ Y) /\ (dom (h1 + h2)) & r2 in (X /\ Y) /\ (dom (h1 + h2)) & r1 < r2 ) ; :: thesis: (h1 + h2) . r2 <= (h1 + h2) . r1
then A21: ( r1 in X /\ (dom h1) & r1 in Y /\ (dom h2) ) by Th68;
A22: ( r2 in X /\ (dom h1) & r2 in Y /\ (dom h2) ) by A20, Th68;
A23: ( r1 in dom (h1 + h2) & r2 in dom (h1 + h2) & r1 < r2 ) by A20, XBOOLE_0:def 4;
A24: h1 . r2 <= h1 . r1 by A19, A20, A21, A22, Def5;
h2 . r2 <= h2 . r1 by A19, A20, A21, A22, Def5;
then (h1 . r2) + (h2 . r2) <= (h1 . r1) + (h2 . r1) by A24, XREAL_1:9;
then (h1 + h2) . r2 <= (h1 . r1) + (h2 . r1) by A23, VALUED_1:def 1;
hence (h1 + h2) . r2 <= (h1 + h2) . r1 by A23, VALUED_1:def 1; :: thesis: verum

end;

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