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 p in (Y /\ X) /\ (dom h) ; :: thesis: h . p = r1
then ( p in Y /\ X & p in dom h ) by XBOOLE_0:def 4;
then ( p in Y & p in X & p in dom h ) by XBOOLE_0:def 4;
then A3: ( p in Y /\ (dom h) & p in X /\ (dom h) ) by XBOOLE_0:def 4;
( x in Y /\ X & x in dom h ) by A2, XBOOLE_0:def 4;
then ( x in Y & x in X & x in dom h ) by XBOOLE_0:def 4;
then A4: ( x in Y /\ (dom h) & x in X /\ (dom h) ) by XBOOLE_0:def 4;

now

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

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

then A6: h . x <= h . p by A1, A3, A4, Th48;
h . p <= h . x by A1, A3, A4, A5, Th49;
hence h . p = h . x by A6, XXREAL_0:1; :: thesis: verum

end;

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

then A8: h . p <= h . x by A1, A3, A4, Th48;
h . x <= h . p by A1, A3, A4, A7, Th49;
hence h . p = h . x by A8, 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