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 )
proof
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 ;
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
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 ;
then A8: (h1 . r1) + (h2 . r1) < (h1 . r2) + r by A3, A7;
A9: r1 in dom (h1 + h2) by ;
r2 in Y /\ (dom h2) by ;
then (h1 . r1) + (h2 . r1) < (h1 . r2) + (h2 . r2) by A3, A8;
then A10: (h1 + h2) . r1 < (h1 . r2) + (h2 . r2) by ;
r2 in dom (h1 + h2) by ;
hence (h1 + h2) . r1 < (h1 + h2) . r2 by ; :: thesis: verum
end;
hence (h1 + h2) | (X /\ Y) is increasing by Th20; :: thesis: verum
end;
assume that
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 ;
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
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 ;
then h1 . r2 < h1 . r1 by ;
then A17: (h1 . r2) + r < (h1 . r1) + r by XREAL_1:6;
r2 in Y /\ (dom h2) by ;
then A18: (h1 . r2) + (h2 . r2) < (h1 . r1) + r by ;
A19: r2 in dom (h1 + h2) by ;
r1 in Y /\ (dom h2) by ;
then (h1 . r2) + (h2 . r2) < (h1 . r1) + (h2 . r1) by ;
then A20: (h1 + h2) . r2 < (h1 . r1) + (h2 . r1) by ;
r1 in dom (h1 + h2) by ;
hence (h1 + h2) . r2 < (h1 + h2) . r1 by ; :: thesis: verum
end;
hence (h1 + h2) | (X /\ Y) is decreasing by Th21; :: thesis: verum