let X, Y 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 V8()
let h be PartFunc of REAL,REAL; :: thesis: ( h | Y is non-decreasing & h | X is non-increasing implies h | (Y /\ X) is V8() )
assume A1: ( h | Y is non-decreasing & h | X is non-increasing ) ; :: thesis: h | (Y /\ X) is V8()
per cases ( (Y /\ X) /\ (dom h) = {} or (Y /\ X) /\ (dom h) <> {} ) ;
suppose (Y /\ X) /\ (dom h) = {} ; :: thesis: h | (Y /\ X) is V8()
then Y /\ X misses dom h ;
hence h | (Y /\ X) is V8() by PARTFUN2:39; :: thesis: verum
end;
suppose A2: (Y /\ X) /\ (dom h) <> {} ; :: thesis: h | (Y /\ X) is V8()
set x = the Element of (Y /\ X) /\ (dom h);
the Element of (Y /\ X) /\ (dom h) in dom h by A2, XBOOLE_0:def 4;
then reconsider x = the Element of (Y /\ X) /\ (dom h) as Element of REAL ;
now :: thesis: ex r1 being Element of REAL st
for p being Element of REAL st p in (Y /\ X) /\ (dom h) holds
h . p = r1
reconsider r1 = h . x as Element of REAL by XREAL_0:def 1;
take r1 = r1; :: thesis: for p being Element of REAL st p in (Y /\ X) /\ (dom h) holds
h . p = r1
now :: thesis: for p being Element of REAL st p in (Y /\ X) /\ (dom h) holds
h . p = h . x
let p be Element of REAL ; :: thesis: ( p in (Y /\ X) /\ (dom h) implies h . b1 = h . x )
assume A3: p in (Y /\ X) /\ (dom h) ; :: thesis: h . b1 = h . x
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;
per cases ( x <= p or p <= x ) ;
suppose x <= p ; :: thesis: h . b1 = h . x
then ( h . x <= h . p & h . p <= h . x ) by A1, A11, A6, A9, A10, Th24, Th25;
hence h . p = h . x by XXREAL_0:1; :: thesis: verum
end;
suppose p <= x ; :: thesis: h . b1 = h . x
then ( h . p <= h . x & h . x <= h . p ) by A1, A11, A6, A9, A10, Th24, Th25;
hence h . p = h . x by XXREAL_0:1; :: thesis: verum
end;
end;
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 V8() by PARTFUN2:57; :: thesis: verum
end;
end;