let X, Y be set ; :: thesis: for h1, h2 being PartFunc of REAL,REAL st h1 | X is non-increasing & h2 | Y is V8() holds
(h1 + h2) | (X /\ Y) is non-increasing

let h1, h2 be PartFunc of REAL,REAL; :: thesis: ( h1 | X is non-increasing & h2 | Y is V8() implies (h1 + h2) | (X /\ Y) is non-increasing )
assume that
A1: h1 | X is non-increasing and
A2: h2 | Y is V8() ; :: thesis: (h1 + h2) | (X /\ Y) is non-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) . 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
A3: r1 in (X /\ Y) /\ (dom (h1 + h2)) and
A4: r2 in (X /\ Y) /\ (dom (h1 + h2)) and
A5: r1 < r2 ; :: thesis: (h1 + h2) . r2 <= (h1 + h2) . r1
A6: r2 in X /\ Y by ;
then A7: r2 in X by XBOOLE_0:def 4;
A8: r2 in Y by ;
A9: r2 in dom (h1 + h2) by ;
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 ;
r2 in dom h1 by ;
then A12: r2 in X /\ (dom h1) by ;
A13: r1 in X /\ Y by ;
then A14: r1 in X by XBOOLE_0:def 4;
A15: r1 in Y by ;
A16: r1 in dom (h1 + h2) by ;
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 ;
then A18: h2 . r2 = h2 . r1 by ;
r1 in dom h1 by ;
then r1 in X /\ (dom h1) by ;
then h1 . r2 <= h1 . r1 by A1, A5, A12, Th23;
then (h1 . r2) + (h2 . r2) <= (h1 . r1) + (h2 . r1) by ;
then (h1 + h2) . r2 <= (h1 . r1) + (h2 . r1) by ;
hence (h1 + h2) . r2 <= (h1 + h2) . r1 by ; :: thesis: verum
end;
hence (h1 + h2) | (X /\ Y) is non-increasing by Th23; :: thesis: verum