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

(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

hence
(h1 + h2) | (X /\ Y) is increasing
by Th20; :: thesis: verum(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 A4, XBOOLE_0:def 4;

then A7: r2 in Y by XBOOLE_0:def 4;

A8: r2 in dom (h1 + h2) by A4, XBOOLE_0:def 4;

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 A7, XBOOLE_0:def 4;

A11: r1 in X /\ Y by A3, XBOOLE_0:def 4;

then A12: r1 in Y by XBOOLE_0:def 4;

A13: r1 in dom (h1 + h2) by A3, XBOOLE_0:def 4;

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 A12, XBOOLE_0:def 4;

then A15: h2 . r1 <= h2 . r2 by A2, A5, A10, Th22;

A16: r2 in X by A6, XBOOLE_0:def 4;

A17: r1 in X by A11, XBOOLE_0:def 4;

r2 in dom h1 by A9, XBOOLE_0:def 4;

then A18: r2 in X /\ (dom h1) by A16, XBOOLE_0:def 4;

r1 in dom h1 by A14, XBOOLE_0:def 4;

then r1 in X /\ (dom h1) by A17, XBOOLE_0:def 4;

then h1 . r1 < h1 . r2 by A1, A5, A18, Th20;

then (h1 . r1) + (h2 . r1) < (h1 . r2) + (h2 . r2) by A15, XREAL_1:8;

then (h1 + h2) . r1 < (h1 . r2) + (h2 . r2) by A13, VALUED_1:def 1;

hence (h1 + h2) . r1 < (h1 + h2) . r2 by A8, VALUED_1:def 1; :: thesis: verum

end;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 A4, XBOOLE_0:def 4;

then A7: r2 in Y by XBOOLE_0:def 4;

A8: r2 in dom (h1 + h2) by A4, XBOOLE_0:def 4;

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 A7, XBOOLE_0:def 4;

A11: r1 in X /\ Y by A3, XBOOLE_0:def 4;

then A12: r1 in Y by XBOOLE_0:def 4;

A13: r1 in dom (h1 + h2) by A3, XBOOLE_0:def 4;

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 A12, XBOOLE_0:def 4;

then A15: h2 . r1 <= h2 . r2 by A2, A5, A10, Th22;

A16: r2 in X by A6, XBOOLE_0:def 4;

A17: r1 in X by A11, XBOOLE_0:def 4;

r2 in dom h1 by A9, XBOOLE_0:def 4;

then A18: r2 in X /\ (dom h1) by A16, XBOOLE_0:def 4;

r1 in dom h1 by A14, XBOOLE_0:def 4;

then r1 in X /\ (dom h1) by A17, XBOOLE_0:def 4;

then h1 . r1 < h1 . r2 by A1, A5, A18, Th20;

then (h1 . r1) + (h2 . r1) < (h1 . r2) + (h2 . r2) by A15, XREAL_1:8;

then (h1 + h2) . r1 < (h1 . r2) + (h2 . r2) by A13, VALUED_1:def 1;

hence (h1 + h2) . r1 < (h1 + h2) . r2 by A8, VALUED_1:def 1; :: thesis: verum