let X, Y be set ; :: thesis: for h1, h2 being PartFunc of REAL,REAL holds

( ( h1 | X is increasing & h2 | Y is V8() implies (h1 + h2) | (X /\ Y) is increasing ) & ( h1 | X is decreasing & h2 | Y is V8() implies (h1 + h2) | (X /\ Y) is decreasing ) )

let h1, h2 be PartFunc of REAL,REAL; :: thesis: ( ( h1 | X is increasing & h2 | Y is V8() implies (h1 + h2) | (X /\ Y) is increasing ) & ( h1 | X is decreasing & h2 | Y is V8() implies (h1 + h2) | (X /\ Y) is decreasing ) )

thus ( h1 | X is increasing & h2 | Y is V8() implies (h1 + h2) | (X /\ Y) is increasing ) :: thesis: ( h1 | X is decreasing & h2 | Y is V8() implies (h1 + h2) | (X /\ Y) is decreasing )

A11: h1 | X is decreasing and

A12: h2 | Y is V8() ; :: thesis: (h1 + h2) | (X /\ Y) is decreasing

consider r being Element of REAL such that

A13: for p being Element of REAL st p in Y /\ (dom h2) holds

h2 . p = r by A12, PARTFUN2:57;

( ( h1 | X is increasing & h2 | Y is V8() implies (h1 + h2) | (X /\ Y) is increasing ) & ( h1 | X is decreasing & h2 | Y is V8() implies (h1 + h2) | (X /\ Y) is decreasing ) )

let h1, h2 be PartFunc of REAL,REAL; :: thesis: ( ( h1 | X is increasing & h2 | Y is V8() implies (h1 + h2) | (X /\ Y) is increasing ) & ( h1 | X is decreasing & h2 | Y is V8() implies (h1 + h2) | (X /\ Y) is decreasing ) )

thus ( h1 | X is increasing & h2 | Y is V8() implies (h1 + h2) | (X /\ Y) is increasing ) :: thesis: ( h1 | X is decreasing & h2 | Y is V8() implies (h1 + h2) | (X /\ Y) is decreasing )

proof

assume that
assume that

A1: h1 | X is increasing and

A2: h2 | Y is V8() ; :: thesis: (h1 + h2) | (X /\ Y) is increasing

consider r being Element of REAL such that

A3: for p being Element of REAL st p in Y /\ (dom h2) holds

h2 . p = r by A2, PARTFUN2:57;

end;A1: h1 | X is increasing and

A2: h2 | Y is V8() ; :: thesis: (h1 + h2) | (X /\ Y) is increasing

consider r being Element of REAL such that

A3: for p being Element of REAL st p in Y /\ (dom h2) holds

h2 . p = r by A2, PARTFUN2:57;

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

A4: r1 in (X /\ Y) /\ (dom (h1 + h2)) and

A5: r2 in (X /\ Y) /\ (dom (h1 + h2)) and

A6: r1 < r2 ; :: thesis: (h1 + h2) . r1 < (h1 + h2) . r2

( r1 in X /\ (dom h1) & r2 in X /\ (dom h1) ) by A4, A5, Th36;

then h1 . r1 < h1 . r2 by A1, A6, Th20;

then A7: (h1 . r1) + r < (h1 . r2) + r by XREAL_1:6;

r1 in Y /\ (dom h2) by A4, Th36;

then A8: (h1 . r1) + (h2 . r1) < (h1 . r2) + r by A3, A7;

A9: r1 in dom (h1 + h2) by A4, XBOOLE_0:def 4;

r2 in Y /\ (dom h2) by A5, Th36;

then (h1 . r1) + (h2 . r1) < (h1 . r2) + (h2 . r2) by A3, A8;

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

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

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

end;assume that

A4: r1 in (X /\ Y) /\ (dom (h1 + h2)) and

A5: r2 in (X /\ Y) /\ (dom (h1 + h2)) and

A6: r1 < r2 ; :: thesis: (h1 + h2) . r1 < (h1 + h2) . r2

( r1 in X /\ (dom h1) & r2 in X /\ (dom h1) ) by A4, A5, Th36;

then h1 . r1 < h1 . r2 by A1, A6, Th20;

then A7: (h1 . r1) + r < (h1 . r2) + r by XREAL_1:6;

r1 in Y /\ (dom h2) by A4, Th36;

then A8: (h1 . r1) + (h2 . r1) < (h1 . r2) + r by A3, A7;

A9: r1 in dom (h1 + h2) by A4, XBOOLE_0:def 4;

r2 in Y /\ (dom h2) by A5, Th36;

then (h1 . r1) + (h2 . r1) < (h1 . r2) + (h2 . r2) by A3, A8;

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

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

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

A11: h1 | X is decreasing and

A12: h2 | Y is V8() ; :: thesis: (h1 + h2) | (X /\ Y) is decreasing

consider r being Element of REAL such that

A13: for p being Element of REAL st p in Y /\ (dom h2) holds

h2 . p = r by A12, PARTFUN2:57;

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) . r2 < (h1 + h2) . r1

hence
(h1 + h2) | (X /\ Y) is decreasing
by Th21; :: thesis: verum(h1 + h2) . r2 < (h1 + h2) . r1

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) . r2 < (h1 + h2) . r1 )

assume that

A14: r1 in (X /\ Y) /\ (dom (h1 + h2)) and

A15: r2 in (X /\ Y) /\ (dom (h1 + h2)) and

A16: r1 < r2 ; :: thesis: (h1 + h2) . r2 < (h1 + h2) . r1

( r1 in X /\ (dom h1) & r2 in X /\ (dom h1) ) by A14, A15, Th36;

then h1 . r2 < h1 . r1 by A11, A16, Th21;

then A17: (h1 . r2) + r < (h1 . r1) + r by XREAL_1:6;

r2 in Y /\ (dom h2) by A15, Th36;

then A18: (h1 . r2) + (h2 . r2) < (h1 . r1) + r by A13, A17;

A19: r2 in dom (h1 + h2) by A15, XBOOLE_0:def 4;

r1 in Y /\ (dom h2) by A14, Th36;

then (h1 . r2) + (h2 . r2) < (h1 . r1) + (h2 . r1) by A13, A18;

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

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

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

end;assume that

A14: r1 in (X /\ Y) /\ (dom (h1 + h2)) and

A15: r2 in (X /\ Y) /\ (dom (h1 + h2)) and

A16: r1 < r2 ; :: thesis: (h1 + h2) . r2 < (h1 + h2) . r1

( r1 in X /\ (dom h1) & r2 in X /\ (dom h1) ) by A14, A15, Th36;

then h1 . r2 < h1 . r1 by A11, A16, Th21;

then A17: (h1 . r2) + r < (h1 . r1) + r by XREAL_1:6;

r2 in Y /\ (dom h2) by A15, Th36;

then A18: (h1 . r2) + (h2 . r2) < (h1 . r1) + r by A13, A17;

A19: r2 in dom (h1 + h2) by A15, XBOOLE_0:def 4;

r1 in Y /\ (dom h2) by A14, Th36;

then (h1 . r2) + (h2 . r2) < (h1 . r1) + (h2 . r1) by A13, A18;

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

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

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