let Y, X be set ; :: thesis: for h being PartFunc of REAL ,REAL st h | Y is non-decreasing & h | X is non-increasing holds
h | (Y /\ X) is constant
let h be PartFunc of REAL ,REAL ; :: thesis: ( h | Y is non-decreasing & h | X is non-increasing implies h | (Y /\ X) is constant )
assume A1: ( h | Y is non-decreasing & h | X is non-increasing ) ; :: thesis: h | (Y /\ X) is constant

now

per cases ( (Y /\ X) /\ (dom h) = {} or (Y /\ X) /\ (dom h) <> {} ) ;

suppose (Y /\ X) /\ (dom h) = {} ; :: thesis: h | (Y /\ X) is constant

then Y /\ X misses dom h by XBOOLE_0:def 7;
hence h | (Y /\ X) is constant by PARTFUN2:58; :: thesis: verum

end;

suppose A2: (Y /\ X) /\ (dom h) <> {} ; :: thesis: h | (Y /\ X) is constant

consider x being Element of (Y /\ X) /\ (dom h);
x in dom h by A2, XBOOLE_0:def 4;
then reconsider x = x as Real ;

now

take r1 = h . x; :: thesis: for p being Element of REAL st p in (Y /\ X) /\ (dom h) holds
h . p = r1

now

let p be Element of REAL ; :: thesis: ( p in (Y /\ X) /\ (dom h) implies h . p = r1 )
assume A3: p in (Y /\ X) /\ (dom h) ; :: thesis: h . p = r1
then A4: p in Y /\ X by XBOOLE_0:def 4;
A5: p in dom h by A3, XBOOLE_0:def 4;
p in X by A4, XBOOLE_0:def 4;
then A6: p in X /\ (dom h) by A5, XBOOLE_0:def 4;
A7: x in dom h by A2, XBOOLE_0:def 4;
A8: x in Y /\ X by A2, XBOOLE_0:def 4;
then x in Y by XBOOLE_0:def 4;
then A9: x in Y /\ (dom h) by A7, XBOOLE_0:def 4;
x in X by A8, XBOOLE_0:def 4;
then A10: x in X /\ (dom h) by A7, XBOOLE_0:def 4;
p in Y by A4, XBOOLE_0:def 4;
then A11: p in Y /\ (dom h) by A5, XBOOLE_0:def 4;

now

per cases ( x <= p or p <= x ) ;

suppose x <= p ; :: thesis: h . p = h . x

then ( h . x <= h . p & h . p <= h . x ) by A1, A11, A6, A9, A10, Th48, Th49;
hence h . p = h . x by XXREAL_0:1; :: thesis: verum

end;

suppose p <= x ; :: thesis: h . p = h . x

then ( h . p <= h . x & h . x <= h . p ) by A1, A11, A6, A9, A10, Th48, Th49;
hence h . p = h . x by XXREAL_0:1; :: thesis: verum

end;

end;

end;

hence h . p = r1 ; :: thesis: verum

end;

hence for p being Element of REAL st p in (Y /\ X) /\ (dom h) holds
h . p = r1 ; :: thesis: verum

end;

hence h | (Y /\ X) is constant by PARTFUN2:76; :: thesis: verum

end;

end;

end;

hence h | (Y /\ X) is constant ; :: thesis: verum