let X, Y be set ; 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; ( 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 )
; h | (Y /\ X) is V8()
per cases
( (Y /\ X) /\ (dom h) = {} or (Y /\ X) /\ (dom h) <> {} )
;
suppose A2:
(Y /\ X) /\ (dom h) <> {}
;
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 ex r1 being Element of REAL st
for p being Element of REAL st p in (Y /\ X) /\ (dom h) holds
h . p = r1reconsider r1 =
h . x as
Element of
REAL by XREAL_0:def 1;
take r1 =
r1;
for p being Element of REAL st p in (Y /\ X) /\ (dom h) holds
h . p = r1now for p being Element of REAL st p in (Y /\ X) /\ (dom h) holds
h . p = h . xlet p be
Element of
REAL ;
( p in (Y /\ X) /\ (dom h) implies h . b1 = h . x )assume A3:
p in (Y /\ X) /\ (dom h)
;
h . b1 = h . xthen 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;
end; hence
for
p being
Element of
REAL st
p in (Y /\ X) /\ (dom h) holds
h . p = r1
;
verum end; hence
h | (Y /\ X) is
V8()
by PARTFUN2:57;
verum end; end;