let X, Y be set ; for h1, h2 being PartFunc of REAL,REAL st h1 | X is non-decreasing & h2 | Y is constant holds
(h1 + h2) | (X /\ Y) is non-decreasing
let h1, h2 be PartFunc of REAL,REAL; ( h1 | X is non-decreasing & h2 | Y is constant implies (h1 + h2) | (X /\ Y) is non-decreasing )
assume that
A1:
h1 | X is non-decreasing
and
A2:
h2 | Y is constant
; (h1 + h2) | (X /\ Y) is non-decreasing
now 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) . r2let r1,
r2 be
Real;
( 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
;
(h1 + h2) . r1 <= (h1 + h2) . r2A6:
r2 in X /\ Y
by A4, XBOOLE_0:def 4;
then A7:
r2 in X
by XBOOLE_0:def 4;
A8:
r2 in Y
by A6, XBOOLE_0:def 4;
A9:
r2 in dom (h1 + h2)
by A4, XBOOLE_0:def 4;
then A10:
r2 in (dom h1) /\ (dom h2)
by VALUED_1:def 1;
then
r2 in dom h2
by XBOOLE_0:def 4;
then A11:
r2 in Y /\ (dom h2)
by A8, XBOOLE_0:def 4;
r2 in dom h1
by A10, XBOOLE_0:def 4;
then A12:
r2 in X /\ (dom h1)
by A7, XBOOLE_0:def 4;
A13:
r1 in X /\ Y
by A3, XBOOLE_0:def 4;
then A14:
r1 in X
by XBOOLE_0:def 4;
A15:
r1 in Y
by A13, XBOOLE_0:def 4;
A16:
r1 in dom (h1 + h2)
by A3, XBOOLE_0:def 4;
then A17:
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 A15, XBOOLE_0:def 4;
then A18:
h2 . r2 = h2 . r1
by A2, A11, PARTFUN2:58;
r1 in dom h1
by A17, XBOOLE_0:def 4;
then
r1 in X /\ (dom h1)
by A14, XBOOLE_0:def 4;
then
h1 . r1 <= h1 . r2
by A1, A5, A12, Th22;
then
(h1 . r1) + (h2 . r1) <= (h1 . r2) + (h2 . r2)
by A18, XREAL_1:6;
then
(h1 + h2) . r1 <= (h1 . r2) + (h2 . r2)
by A16, VALUED_1:def 1;
hence
(h1 + h2) . r1 <= (h1 + h2) . r2
by A9, VALUED_1:def 1;
verum end;
hence
(h1 + h2) | (X /\ Y) is non-decreasing
by Th22; verum