let X, Y be set ; for h1, h2 being PartFunc of REAL,REAL st h1 | X is decreasing & h2 | Y is non-increasing holds
(h1 + h2) | (X /\ Y) is decreasing
let h1, h2 be PartFunc of REAL,REAL; ( h1 | X is decreasing & h2 | Y is non-increasing implies (h1 + h2) | (X /\ Y) is decreasing )
assume that
A1:
h1 | X is decreasing
and
A2:
h2 | Y is non-increasing
; (h1 + h2) | (X /\ Y) is 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) . r2 < (h1 + h2) . r1let r1,
r2 be
Real;
( r1 in (X /\ Y) /\ (dom (h1 + h2)) & r2 in (X /\ Y) /\ (dom (h1 + h2)) & r1 < r2 implies (h1 + h2) . r2 < (h1 + h2) . r1 )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) . r2 < (h1 + h2) . r1A6:
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 . r2 <= h2 . r1
by A2, A5, A10, Th23;
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 . r2 < h1 . r1
by A1, A5, A18, Th21;
then
(h1 . r2) + (h2 . r2) < (h1 . r1) + (h2 . r1)
by A15, XREAL_1:8;
then
(h1 + h2) . r2 < (h1 . r1) + (h2 . r1)
by A8, VALUED_1:def 1;
hence
(h1 + h2) . r2 < (h1 + h2) . r1
by A13, VALUED_1:def 1;
verum end;
hence
(h1 + h2) | (X /\ Y) is decreasing
by Th21; verum