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 that
A1: h1 | X is increasing and
A2: h2 | Y is non-decreasing ; :: 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
A6: r2 in X /\ Y by ;
then A7: r2 in Y by XBOOLE_0:def 4;
A8: r2 in dom (h1 + h2) by ;
then A9: r2 in (dom h1) /\ (dom h2) by VALUED_1:def 1;
then r2 in dom h2 by XBOOLE_0:def 4;
then A10: r2 in Y /\ (dom h2) by ;
A11: r1 in X /\ Y by ;
then A12: r1 in Y by XBOOLE_0:def 4;
A13: r1 in dom (h1 + h2) by ;
then A14: r1 in (dom h1) /\ (dom h2) by VALUED_1:def 1;
then r1 in dom h2 by XBOOLE_0:def 4;
then r1 in Y /\ (dom h2) by ;
then A15: h2 . r1 <= h2 . r2 by A2, A5, A10, Th22;
A16: r2 in X by ;
A17: r1 in X by ;
r2 in dom h1 by ;
then A18: r2 in X /\ (dom h1) by ;
r1 in dom h1 by ;
then r1 in X /\ (dom h1) by ;
then h1 . r1 < h1 . r2 by A1, A5, A18, Th20;
then (h1 . r1) + (h2 . r1) < (h1 . r2) + (h2 . r2) by ;
then (h1 + h2) . r1 < (h1 . r2) + (h2 . r2) by ;
hence (h1 + h2) . r1 < (h1 + h2) . r2 by ; :: thesis: verum
end;
hence (h1 + h2) | (X /\ Y) is increasing by Th20; :: thesis: verum