let X, Y be set ; :: thesis: for h1, h2 being PartFunc of REAL ,REAL st h1 | X is increasing & h2 | Y is non-decreasing holds
(h1 + h2) | (X /\ Y) is increasing
let h1, h2 be PartFunc of REAL ,REAL ; :: thesis: ( h1 | X is increasing & h2 | Y is non-decreasing implies (h1 + h2) | (X /\ Y) is increasing )
assume A1: ( h1 | X is increasing & h2 | Y is non-decreasing ) ; :: 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 /\ Y & r1 in dom (h1 + h2) & r2 in X /\ Y & r2 in dom (h1 + h2) ) by XBOOLE_0:def 4;
then A4: ( r1 in X & r1 in Y & r2 in X & r2 in Y ) by XBOOLE_0:def 4;
( r1 in (dom h1) /\ (dom h2) & r2 in (dom h1) /\ (dom h2) ) by A3, VALUED_1:def 1;
then A5: ( r1 in dom h1 & r1 in dom h2 & r2 in dom h1 & r2 in dom h2 ) by XBOOLE_0:def 4;
then ( r1 in X /\ (dom h1) & r2 in X /\ (dom h1) ) by A4, XBOOLE_0:def 4;
then A6: h1 . r1 < h1 . r2 by A1, A2, Def2;
( r1 in Y /\ (dom h2) & r2 in Y /\ (dom h2) ) by A4, A5, XBOOLE_0:def 4;
then h2 . r1 <= h2 . r2 by A1, A2, Def4;
then (h1 . r1) + (h2 . r1) < (h1 . r2) + (h2 . r2) by A6, XREAL_1:10;
then (h1 + h2) . r1 < (h1 . r2) + (h2 . r2) by A3, VALUED_1:def 1;
hence (h1 + h2) . r1 < (h1 + h2) . r2 by A3, VALUED_1:def 1; :: thesis: verum

end;

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