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 A1: ( h1 | X is increasing & h2 | Y is constant ) ; :: thesis: (h1 + h2) | (X /\ Y) is increasing
then consider r being Element of REAL such that
A2: for p being Element of REAL st p in Y /\ (dom h2) holds
h2 . p = r by PARTFUN2:76;

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

end;

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

end;

assume A7: ( h1 | X is decreasing & h2 | Y is constant ) ; :: thesis: (h1 + h2) | (X /\ Y) is decreasing
then consider r being Element of REAL such that
A8: for p being Element of REAL st p in Y /\ (dom h2) holds
h2 . p = r by PARTFUN2:76;

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

end;

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