let X be set ; :: thesis: for f being PartFunc of REAL,REAL st f | X is monotone & ex p, g being Real st

( p <= g & f .: X = [.p,g.] ) holds

f | X is continuous

let f be PartFunc of REAL,REAL; :: thesis: ( f | X is monotone & ex p, g being Real st

( p <= g & f .: X = [.p,g.] ) implies f | X is continuous )

assume A1: f | X is monotone ; :: thesis: ( for p, g being Real holds

( not p <= g or not f .: X = [.p,g.] ) or f | X is continuous )

given p, g being Real such that A2: p <= g and

A3: f .: X = [.p,g.] ; :: thesis: f | X is continuous

reconsider p = p, g = g as Real ;

( p <= g & f .: X = [.p,g.] ) holds

f | X is continuous

let f be PartFunc of REAL,REAL; :: thesis: ( f | X is monotone & ex p, g being Real st

( p <= g & f .: X = [.p,g.] ) implies f | X is continuous )

assume A1: f | X is monotone ; :: thesis: ( for p, g being Real holds

( not p <= g or not f .: X = [.p,g.] ) or f | X is continuous )

given p, g being Real such that A2: p <= g and

A3: f .: X = [.p,g.] ; :: thesis: f | X is continuous

reconsider p = p, g = g as Real ;

now :: thesis: f | X is continuous end;

hence
f | X is continuous
; :: thesis: verumper cases
( p = g or p < g )
by A2, XXREAL_0:1;

end;

suppose
p = g
; :: thesis: f | X is continuous

then
f .: X = {p}
by A3, XXREAL_1:17;

then rng (f | X) = {p} by RELAT_1:115;

then f | X is V8() ;

hence f | X is continuous ; :: thesis: verum

end;then rng (f | X) = {p} by RELAT_1:115;

then f | X is V8() ;

hence f | X is continuous ; :: thesis: verum

suppose A4:
p < g
; :: thesis: f | X is continuous

end;

now :: thesis: f | X is continuous end;

hence
f | X is continuous
; :: thesis: verumper cases
( f | X is non-decreasing or f | X is non-increasing )
by A1, RFUNCT_2:def 5;

end;

suppose
f | X is non-decreasing
; :: thesis: f | X is continuous

then A5:
(f | X) | X is non-decreasing
;

for x0 being Real st x0 in dom (f | X) holds

f | X is_continuous_in x0

end;for x0 being Real st x0 in dom (f | X) holds

f | X is_continuous_in x0

proof

hence
f | X is continuous
; :: thesis: verum
A6:
[.p,g.] = ].p,g.[ \/ {p,g}
by A2, XXREAL_1:128;

let x0 be Real; :: thesis: ( x0 in dom (f | X) implies f | X is_continuous_in x0 )

A7: (f | X) .: X = f .: X by RELAT_1:129;

assume A8: x0 in dom (f | X) ; :: thesis: f | X is_continuous_in x0

A9: (f | X) . x0 in (f | X) .: X by A8, FUNCT_1:def 6;

reconsider x0 = x0 as Real ;

(f | X) . x0 in [.p,g.] by A3, A9, RELAT_1:129;

then A10: ( (f | X) . x0 in ].p,g.[ or (f | X) . x0 in {p,g} ) by A6, XBOOLE_0:def 3;

end;let x0 be Real; :: thesis: ( x0 in dom (f | X) implies f | X is_continuous_in x0 )

A7: (f | X) .: X = f .: X by RELAT_1:129;

assume A8: x0 in dom (f | X) ; :: thesis: f | X is_continuous_in x0

A9: (f | X) . x0 in (f | X) .: X by A8, FUNCT_1:def 6;

reconsider x0 = x0 as Real ;

(f | X) . x0 in [.p,g.] by A3, A9, RELAT_1:129;

then A10: ( (f | X) . x0 in ].p,g.[ or (f | X) . x0 in {p,g} ) by A6, XBOOLE_0:def 3;

now :: thesis: for N1 being Neighbourhood of (f | X) . x0 ex N being Neighbourhood of x0 st

for x1 being Real st x1 in dom (f | X) & x1 in N holds

(f | X) . x1 in N1

hence
f | X is_continuous_in x0
by Th4; :: thesis: verumfor x1 being Real st x1 in dom (f | X) & x1 in N holds

(f | X) . x1 in N1

let N1 be Neighbourhood of (f | X) . x0; :: thesis: ex N being Neighbourhood of x0 st

for x1 being Real st x1 in dom (f | X) & x1 in N holds

(f | X) . x1 in N1

A89: for x1 being Real st x1 in dom (f | X) & x1 in N holds

(f | X) . x1 in N1 ;

take N = N; :: thesis: for x1 being Real st x1 in dom (f | X) & x1 in N holds

(f | X) . x1 in N1

thus for x1 being Real st x1 in dom (f | X) & x1 in N holds

(f | X) . x1 in N1 by A89; :: thesis: verum

end;for x1 being Real st x1 in dom (f | X) & x1 in N holds

(f | X) . x1 in N1

now :: thesis: ex N being Neighbourhood of x0 st

for x being Real st x in dom (f | X) & x in N holds

(f | X) . x in N1end;

then consider N being Neighbourhood of x0 such that for x being Real st x in dom (f | X) & x in N holds

(f | X) . x in N1

per cases
( (f | X) . x0 in ].p,g.[ or (f | X) . x0 = p or (f | X) . x0 = g )
by A10, TARSKI:def 2;

end;

suppose
(f | X) . x0 in ].p,g.[
; :: thesis: ex N being Neighbourhood of x0 st

for x being Real st x in dom (f | X) & x in N holds

(f | X) . x in N1

for x being Real st x in dom (f | X) & x in N holds

(f | X) . x in N1

then consider N2 being Neighbourhood of (f | X) . x0 such that

A11: N2 c= ].p,g.[ by RCOMP_1:18;

A12: ].p,g.[ c= [.p,g.] by XXREAL_1:25;

consider N3 being Neighbourhood of (f | X) . x0 such that

A13: N3 c= N1 and

A14: N3 c= N2 by RCOMP_1:17;

consider r being Real such that

A15: r > 0 and

A16: N3 = ].(((f | X) . x0) - r),(((f | X) . x0) + r).[ by RCOMP_1:def 6;

reconsider r = r as Real ;

A17: ((f | X) . x0) + (r / 2) < (((f | X) . x0) + (r / 2)) + (r / 2) by A15, XREAL_1:29, XREAL_1:215;

set M2 = ((f | X) . x0) + (r / 2);

A18: (f | X) . x0 < ((f | X) . x0) + (r / 2) by A15, XREAL_1:29, XREAL_1:215;

A19: (f | X) . x0 < ((f | X) . x0) + r by A15, XREAL_1:29;

then ((f | X) . x0) - r < (((f | X) . x0) + r) - r by XREAL_1:9;

then ((f | X) . x0) - r < ((f | X) . x0) + (r / 2) by A18, XXREAL_0:2;

then ((f | X) . x0) + (r / 2) in { s where s is Real : ( ((f | X) . x0) - r < s & s < ((f | X) . x0) + r ) } by A17;

then A20: ((f | X) . x0) + (r / 2) in ].(((f | X) . x0) - r),(((f | X) . x0) + r).[ by RCOMP_1:def 2;

then ((f | X) . x0) + (r / 2) in N2 by A14, A16;

then ((f | X) . x0) + (r / 2) in ].p,g.[ by A11;

then consider x2 being Element of REAL such that

A21: ( x2 in dom (f | X) & x2 in X ) and

A22: ((f | X) . x0) + (r / 2) = (f | X) . x2 by A3, A7, A12, PARTFUN2:59;

A23: ].p,g.[ c= [.p,g.] by XXREAL_1:25;

set M1 = ((f | X) . x0) - (r / 2);

A24: ((f | X) . x0) - r < (((f | X) . x0) - r) + (r / 2) by A15, XREAL_1:29, XREAL_1:215;

((f | X) . x0) - (r / 2) < (f | X) . x0 by A18, XREAL_1:19;

then ((f | X) . x0) - (r / 2) < ((f | X) . x0) + r by A19, XXREAL_0:2;

then ((f | X) . x0) - (r / 2) in { s where s is Real : ( ((f | X) . x0) - r < s & s < ((f | X) . x0) + r ) } by A24;

then A25: ((f | X) . x0) - (r / 2) in ].(((f | X) . x0) - r),(((f | X) . x0) + r).[ by RCOMP_1:def 2;

then ((f | X) . x0) - (r / 2) in N2 by A14, A16;

then ((f | X) . x0) - (r / 2) in ].p,g.[ by A11;

then consider x1 being Element of REAL such that

A26: ( x1 in dom (f | X) & x1 in X ) and

A27: ((f | X) . x0) - (r / 2) = (f | X) . x1 by A3, A7, A23, PARTFUN2:59;

A28: (f | X) . x0 < ((f | X) . x0) + (r / 2) by A15, XREAL_1:29, XREAL_1:215;

then A29: ((f | X) . x0) - (r / 2) < (f | X) . x0 by XREAL_1:19;

then x0 < x2 by A33, XXREAL_0:1;

then A35: x2 - x0 > 0 by XREAL_1:50;

set R = min ((x0 - x1),(x2 - x0));

A36: min ((x0 - x1),(x2 - x0)) <= x2 - x0 by XXREAL_0:17;

x1 <> x0 by A27, A28, XREAL_1:19;

then x1 < x0 by A30, XXREAL_0:1;

then x0 - x1 > 0 by XREAL_1:50;

then min ((x0 - x1),(x2 - x0)) > 0 by A35, XXREAL_0:15;

then reconsider N = ].(x0 - (min ((x0 - x1),(x2 - x0)))),(x0 + (min ((x0 - x1),(x2 - x0)))).[ as Neighbourhood of x0 by RCOMP_1:def 6;

take N = N; :: thesis: for x being Real st x in dom (f | X) & x in N holds

(f | X) . x in N1

let x be Real; :: thesis: ( x in dom (f | X) & x in N implies (f | X) . x in N1 )

assume that

A37: x in dom (f | X) and

A38: x in N ; :: thesis: (f | X) . x in N1

A39: x in X /\ (dom (f | X)) by A37, XBOOLE_1:28;

x in { s where s is Real : ( x0 - (min ((x0 - x1),(x2 - x0))) < s & s < x0 + (min ((x0 - x1),(x2 - x0))) ) } by A38, RCOMP_1:def 2;

then A40: ex s being Real st

( s = x & x0 - (min ((x0 - x1),(x2 - x0))) < s & s < x0 + (min ((x0 - x1),(x2 - x0))) ) ;

then x0 < (min ((x0 - x1),(x2 - x0))) + x by XREAL_1:19;

then A41: x0 - x < ((min ((x0 - x1),(x2 - x0))) + x) - x by XREAL_1:9;

min ((x0 - x1),(x2 - x0)) <= x0 - x1 by XXREAL_0:17;

then x0 - x < x0 - x1 by A41, XXREAL_0:2;

then - (x0 - x) > - (x0 - x1) by XREAL_1:24;

then A42: (x - x0) + x0 > (x1 - x0) + x0 by XREAL_1:6;

x1 in X /\ (dom (f | X)) by A26, XBOOLE_0:def 4;

then A43: (f | X) . x1 <= (f | X) . x by A5, A42, A39, RFUNCT_2:22;

x - x0 < min ((x0 - x1),(x2 - x0)) by A40, XREAL_1:19;

then x - x0 < x2 - x0 by A36, XXREAL_0:2;

then A44: (x - x0) + x0 < (x2 - x0) + x0 by XREAL_1:6;

x2 in X /\ (dom (f | X)) by A21, XBOOLE_0:def 4;

then (f | X) . x <= (f | X) . x2 by A5, A44, A39, RFUNCT_2:22;

then (f | X) . x in { s where s is Real : ( ((f | X) . x0) - (r / 2) <= s & s <= ((f | X) . x0) + (r / 2) ) } by A27, A22, A43;

then A45: (f | X) . x in [.(((f | X) . x0) - (r / 2)),(((f | X) . x0) + (r / 2)).] by RCOMP_1:def 1;

[.(((f | X) . x0) - (r / 2)),(((f | X) . x0) + (r / 2)).] c= ].(((f | X) . x0) - r),(((f | X) . x0) + r).[ by A25, A20, XXREAL_2:def 12;

then (f | X) . x in N3 by A16, A45;

hence (f | X) . x in N1 by A13; :: thesis: verum

end;A11: N2 c= ].p,g.[ by RCOMP_1:18;

A12: ].p,g.[ c= [.p,g.] by XXREAL_1:25;

consider N3 being Neighbourhood of (f | X) . x0 such that

A13: N3 c= N1 and

A14: N3 c= N2 by RCOMP_1:17;

consider r being Real such that

A15: r > 0 and

A16: N3 = ].(((f | X) . x0) - r),(((f | X) . x0) + r).[ by RCOMP_1:def 6;

reconsider r = r as Real ;

A17: ((f | X) . x0) + (r / 2) < (((f | X) . x0) + (r / 2)) + (r / 2) by A15, XREAL_1:29, XREAL_1:215;

set M2 = ((f | X) . x0) + (r / 2);

A18: (f | X) . x0 < ((f | X) . x0) + (r / 2) by A15, XREAL_1:29, XREAL_1:215;

A19: (f | X) . x0 < ((f | X) . x0) + r by A15, XREAL_1:29;

then ((f | X) . x0) - r < (((f | X) . x0) + r) - r by XREAL_1:9;

then ((f | X) . x0) - r < ((f | X) . x0) + (r / 2) by A18, XXREAL_0:2;

then ((f | X) . x0) + (r / 2) in { s where s is Real : ( ((f | X) . x0) - r < s & s < ((f | X) . x0) + r ) } by A17;

then A20: ((f | X) . x0) + (r / 2) in ].(((f | X) . x0) - r),(((f | X) . x0) + r).[ by RCOMP_1:def 2;

then ((f | X) . x0) + (r / 2) in N2 by A14, A16;

then ((f | X) . x0) + (r / 2) in ].p,g.[ by A11;

then consider x2 being Element of REAL such that

A21: ( x2 in dom (f | X) & x2 in X ) and

A22: ((f | X) . x0) + (r / 2) = (f | X) . x2 by A3, A7, A12, PARTFUN2:59;

A23: ].p,g.[ c= [.p,g.] by XXREAL_1:25;

set M1 = ((f | X) . x0) - (r / 2);

A24: ((f | X) . x0) - r < (((f | X) . x0) - r) + (r / 2) by A15, XREAL_1:29, XREAL_1:215;

((f | X) . x0) - (r / 2) < (f | X) . x0 by A18, XREAL_1:19;

then ((f | X) . x0) - (r / 2) < ((f | X) . x0) + r by A19, XXREAL_0:2;

then ((f | X) . x0) - (r / 2) in { s where s is Real : ( ((f | X) . x0) - r < s & s < ((f | X) . x0) + r ) } by A24;

then A25: ((f | X) . x0) - (r / 2) in ].(((f | X) . x0) - r),(((f | X) . x0) + r).[ by RCOMP_1:def 2;

then ((f | X) . x0) - (r / 2) in N2 by A14, A16;

then ((f | X) . x0) - (r / 2) in ].p,g.[ by A11;

then consider x1 being Element of REAL such that

A26: ( x1 in dom (f | X) & x1 in X ) and

A27: ((f | X) . x0) - (r / 2) = (f | X) . x1 by A3, A7, A23, PARTFUN2:59;

A28: (f | X) . x0 < ((f | X) . x0) + (r / 2) by A15, XREAL_1:29, XREAL_1:215;

then A29: ((f | X) . x0) - (r / 2) < (f | X) . x0 by XREAL_1:19;

A30: now :: thesis: not x0 < x1

A32:
((f | X) . x0) + (r / 2) > (f | X) . x0
by A15, XREAL_1:29, XREAL_1:215;assume A31:
x0 < x1
; :: thesis: contradiction

( x0 in X /\ (dom (f | X)) & x1 in X /\ (dom (f | X)) ) by A8, A26, XBOOLE_0:def 4;

hence contradiction by A5, A27, A29, A31, RFUNCT_2:22; :: thesis: verum

end;( x0 in X /\ (dom (f | X)) & x1 in X /\ (dom (f | X)) ) by A8, A26, XBOOLE_0:def 4;

hence contradiction by A5, A27, A29, A31, RFUNCT_2:22; :: thesis: verum

A33: now :: thesis: not x2 < x0

x0 <> x2
by A15, A22, XREAL_1:29, XREAL_1:215;assume A34:
x2 < x0
; :: thesis: contradiction

( x0 in X /\ (dom (f | X)) & x2 in X /\ (dom (f | X)) ) by A8, A21, XBOOLE_0:def 4;

hence contradiction by A5, A22, A32, A34, RFUNCT_2:22; :: thesis: verum

end;( x0 in X /\ (dom (f | X)) & x2 in X /\ (dom (f | X)) ) by A8, A21, XBOOLE_0:def 4;

hence contradiction by A5, A22, A32, A34, RFUNCT_2:22; :: thesis: verum

then x0 < x2 by A33, XXREAL_0:1;

then A35: x2 - x0 > 0 by XREAL_1:50;

set R = min ((x0 - x1),(x2 - x0));

A36: min ((x0 - x1),(x2 - x0)) <= x2 - x0 by XXREAL_0:17;

x1 <> x0 by A27, A28, XREAL_1:19;

then x1 < x0 by A30, XXREAL_0:1;

then x0 - x1 > 0 by XREAL_1:50;

then min ((x0 - x1),(x2 - x0)) > 0 by A35, XXREAL_0:15;

then reconsider N = ].(x0 - (min ((x0 - x1),(x2 - x0)))),(x0 + (min ((x0 - x1),(x2 - x0)))).[ as Neighbourhood of x0 by RCOMP_1:def 6;

take N = N; :: thesis: for x being Real st x in dom (f | X) & x in N holds

(f | X) . x in N1

let x be Real; :: thesis: ( x in dom (f | X) & x in N implies (f | X) . x in N1 )

assume that

A37: x in dom (f | X) and

A38: x in N ; :: thesis: (f | X) . x in N1

A39: x in X /\ (dom (f | X)) by A37, XBOOLE_1:28;

x in { s where s is Real : ( x0 - (min ((x0 - x1),(x2 - x0))) < s & s < x0 + (min ((x0 - x1),(x2 - x0))) ) } by A38, RCOMP_1:def 2;

then A40: ex s being Real st

( s = x & x0 - (min ((x0 - x1),(x2 - x0))) < s & s < x0 + (min ((x0 - x1),(x2 - x0))) ) ;

then x0 < (min ((x0 - x1),(x2 - x0))) + x by XREAL_1:19;

then A41: x0 - x < ((min ((x0 - x1),(x2 - x0))) + x) - x by XREAL_1:9;

min ((x0 - x1),(x2 - x0)) <= x0 - x1 by XXREAL_0:17;

then x0 - x < x0 - x1 by A41, XXREAL_0:2;

then - (x0 - x) > - (x0 - x1) by XREAL_1:24;

then A42: (x - x0) + x0 > (x1 - x0) + x0 by XREAL_1:6;

x1 in X /\ (dom (f | X)) by A26, XBOOLE_0:def 4;

then A43: (f | X) . x1 <= (f | X) . x by A5, A42, A39, RFUNCT_2:22;

x - x0 < min ((x0 - x1),(x2 - x0)) by A40, XREAL_1:19;

then x - x0 < x2 - x0 by A36, XXREAL_0:2;

then A44: (x - x0) + x0 < (x2 - x0) + x0 by XREAL_1:6;

x2 in X /\ (dom (f | X)) by A21, XBOOLE_0:def 4;

then (f | X) . x <= (f | X) . x2 by A5, A44, A39, RFUNCT_2:22;

then (f | X) . x in { s where s is Real : ( ((f | X) . x0) - (r / 2) <= s & s <= ((f | X) . x0) + (r / 2) ) } by A27, A22, A43;

then A45: (f | X) . x in [.(((f | X) . x0) - (r / 2)),(((f | X) . x0) + (r / 2)).] by RCOMP_1:def 1;

[.(((f | X) . x0) - (r / 2)),(((f | X) . x0) + (r / 2)).] c= ].(((f | X) . x0) - r),(((f | X) . x0) + r).[ by A25, A20, XXREAL_2:def 12;

then (f | X) . x in N3 by A16, A45;

hence (f | X) . x in N1 by A13; :: thesis: verum

suppose A46:
(f | X) . x0 = p
; :: thesis: ex N being Neighbourhood of x0 st

for x being Real st x in dom (f | X) & x in N holds

(f | X) . x in N1

for x being Real st x in dom (f | X) & x in N holds

(f | X) . x in N1

then consider r being Real such that

A47: r > 0 and

A48: N1 = ].(p - r),(p + r).[ by RCOMP_1:def 6;

reconsider r = r as Real ;

set R = (min (r,(g - p))) / 2;

g - p > 0 by A4, XREAL_1:50;

then A49: min (r,(g - p)) > 0 by A47, XXREAL_0:15;

then A50: (min (r,(g - p))) / 2 < min (r,(g - p)) by XREAL_1:216;

min (r,(g - p)) <= r by XXREAL_0:17;

then A51: (min (r,(g - p))) / 2 < r by A50, XXREAL_0:2;

then A52: p + ((min (r,(g - p))) / 2) < p + r by XREAL_1:6;

A53: p - ((min (r,(g - p))) / 2) < p by A49, XREAL_1:44, XREAL_1:215;

- r < - ((min (r,(g - p))) / 2) by A51, XREAL_1:24;

then A54: p + (- r) < p + (- ((min (r,(g - p))) / 2)) by XREAL_1:6;

p < p + r by A47, XREAL_1:29;

then p - ((min (r,(g - p))) / 2) < p + r by A53, XXREAL_0:2;

then p - ((min (r,(g - p))) / 2) in { s where s is Real : ( p - r < s & s < p + r ) } by A54;

then A55: p - ((min (r,(g - p))) / 2) in ].(p - r),(p + r).[ by RCOMP_1:def 2;

A56: ].p,g.[ c= [.p,g.] by XXREAL_1:25;

A57: p < p + ((min (r,(g - p))) / 2) by A49, XREAL_1:29, XREAL_1:215;

min (r,(g - p)) <= g - p by XXREAL_0:17;

then (min (r,(g - p))) / 2 < g - p by A50, XXREAL_0:2;

then p + ((min (r,(g - p))) / 2) < g by XREAL_1:20;

then p + ((min (r,(g - p))) / 2) in { s where s is Real : ( p < s & s < g ) } by A57;

then p + ((min (r,(g - p))) / 2) in ].p,g.[ by RCOMP_1:def 2;

then consider x1 being Element of REAL such that

A58: ( x1 in dom (f | X) & x1 in X ) and

A59: p + ((min (r,(g - p))) / 2) = (f | X) . x1 by A3, A7, A56, PARTFUN2:59;

A60: x1 in X /\ (dom (f | X)) by A58, XBOOLE_0:def 4;

then reconsider N = ].(x0 - (x1 - x0)),(x0 + (x1 - x0)).[ as Neighbourhood of x0 by RCOMP_1:def 6, XREAL_1:50;

take N = N; :: thesis: for x being Real st x in dom (f | X) & x in N holds

(f | X) . x in N1

let x be Real; :: thesis: ( x in dom (f | X) & x in N implies (f | X) . x in N1 )

assume that

A62: x in dom (f | X) and

A63: x in N ; :: thesis: (f | X) . x in N1

x in { s where s is Real : ( x0 - (x1 - x0) < s & s < x0 + (x1 - x0) ) } by A63, RCOMP_1:def 2;

then A64: ex s being Real st

( s = x & x0 - (x1 - x0) < s & s < x0 + (x1 - x0) ) ;

(f | X) . x in [.p,g.] by A3, A7, A62, FUNCT_1:def 6;

then (f | X) . x in { s where s is Real : ( p <= s & s <= g ) } by RCOMP_1:def 1;

then ex s being Real st

( s = (f | X) . x & p <= s & s <= g ) ;

then A65: p - ((min (r,(g - p))) / 2) <= (f | X) . x by A53, XXREAL_0:2;

x in X /\ (dom (f | X)) by A62, XBOOLE_0:def 4;

then (f | X) . x <= p + ((min (r,(g - p))) / 2) by A5, A59, A60, A64, RFUNCT_2:22;

then (f | X) . x in { s where s is Real : ( p - ((min (r,(g - p))) / 2) <= s & s <= p + ((min (r,(g - p))) / 2) ) } by A65;

then A66: (f | X) . x in [.(p - ((min (r,(g - p))) / 2)),(p + ((min (r,(g - p))) / 2)).] by RCOMP_1:def 1;

p - r < p by A47, XREAL_1:44;

then p - r < p + ((min (r,(g - p))) / 2) by A57, XXREAL_0:2;

then p + ((min (r,(g - p))) / 2) in { s where s is Real : ( p - r < s & s < p + r ) } by A52;

then p + ((min (r,(g - p))) / 2) in ].(p - r),(p + r).[ by RCOMP_1:def 2;

then [.(p - ((min (r,(g - p))) / 2)),(p + ((min (r,(g - p))) / 2)).] c= N1 by A48, A55, XXREAL_2:def 12;

hence (f | X) . x in N1 by A66; :: thesis: verum

end;A47: r > 0 and

A48: N1 = ].(p - r),(p + r).[ by RCOMP_1:def 6;

reconsider r = r as Real ;

set R = (min (r,(g - p))) / 2;

g - p > 0 by A4, XREAL_1:50;

then A49: min (r,(g - p)) > 0 by A47, XXREAL_0:15;

then A50: (min (r,(g - p))) / 2 < min (r,(g - p)) by XREAL_1:216;

min (r,(g - p)) <= r by XXREAL_0:17;

then A51: (min (r,(g - p))) / 2 < r by A50, XXREAL_0:2;

then A52: p + ((min (r,(g - p))) / 2) < p + r by XREAL_1:6;

A53: p - ((min (r,(g - p))) / 2) < p by A49, XREAL_1:44, XREAL_1:215;

- r < - ((min (r,(g - p))) / 2) by A51, XREAL_1:24;

then A54: p + (- r) < p + (- ((min (r,(g - p))) / 2)) by XREAL_1:6;

p < p + r by A47, XREAL_1:29;

then p - ((min (r,(g - p))) / 2) < p + r by A53, XXREAL_0:2;

then p - ((min (r,(g - p))) / 2) in { s where s is Real : ( p - r < s & s < p + r ) } by A54;

then A55: p - ((min (r,(g - p))) / 2) in ].(p - r),(p + r).[ by RCOMP_1:def 2;

A56: ].p,g.[ c= [.p,g.] by XXREAL_1:25;

A57: p < p + ((min (r,(g - p))) / 2) by A49, XREAL_1:29, XREAL_1:215;

min (r,(g - p)) <= g - p by XXREAL_0:17;

then (min (r,(g - p))) / 2 < g - p by A50, XXREAL_0:2;

then p + ((min (r,(g - p))) / 2) < g by XREAL_1:20;

then p + ((min (r,(g - p))) / 2) in { s where s is Real : ( p < s & s < g ) } by A57;

then p + ((min (r,(g - p))) / 2) in ].p,g.[ by RCOMP_1:def 2;

then consider x1 being Element of REAL such that

A58: ( x1 in dom (f | X) & x1 in X ) and

A59: p + ((min (r,(g - p))) / 2) = (f | X) . x1 by A3, A7, A56, PARTFUN2:59;

A60: x1 in X /\ (dom (f | X)) by A58, XBOOLE_0:def 4;

now :: thesis: not x1 < x0

then
x0 < x1
by A46, A57, A59, XXREAL_0:1;assume A61:
x1 < x0
; :: thesis: contradiction

( x0 in X /\ (dom (f | X)) & x1 in X /\ (dom (f | X)) ) by A8, A58, XBOOLE_0:def 4;

hence contradiction by A5, A46, A57, A59, A61, RFUNCT_2:22; :: thesis: verum

end;( x0 in X /\ (dom (f | X)) & x1 in X /\ (dom (f | X)) ) by A8, A58, XBOOLE_0:def 4;

hence contradiction by A5, A46, A57, A59, A61, RFUNCT_2:22; :: thesis: verum

then reconsider N = ].(x0 - (x1 - x0)),(x0 + (x1 - x0)).[ as Neighbourhood of x0 by RCOMP_1:def 6, XREAL_1:50;

take N = N; :: thesis: for x being Real st x in dom (f | X) & x in N holds

(f | X) . x in N1

let x be Real; :: thesis: ( x in dom (f | X) & x in N implies (f | X) . x in N1 )

assume that

A62: x in dom (f | X) and

A63: x in N ; :: thesis: (f | X) . x in N1

x in { s where s is Real : ( x0 - (x1 - x0) < s & s < x0 + (x1 - x0) ) } by A63, RCOMP_1:def 2;

then A64: ex s being Real st

( s = x & x0 - (x1 - x0) < s & s < x0 + (x1 - x0) ) ;

(f | X) . x in [.p,g.] by A3, A7, A62, FUNCT_1:def 6;

then (f | X) . x in { s where s is Real : ( p <= s & s <= g ) } by RCOMP_1:def 1;

then ex s being Real st

( s = (f | X) . x & p <= s & s <= g ) ;

then A65: p - ((min (r,(g - p))) / 2) <= (f | X) . x by A53, XXREAL_0:2;

x in X /\ (dom (f | X)) by A62, XBOOLE_0:def 4;

then (f | X) . x <= p + ((min (r,(g - p))) / 2) by A5, A59, A60, A64, RFUNCT_2:22;

then (f | X) . x in { s where s is Real : ( p - ((min (r,(g - p))) / 2) <= s & s <= p + ((min (r,(g - p))) / 2) ) } by A65;

then A66: (f | X) . x in [.(p - ((min (r,(g - p))) / 2)),(p + ((min (r,(g - p))) / 2)).] by RCOMP_1:def 1;

p - r < p by A47, XREAL_1:44;

then p - r < p + ((min (r,(g - p))) / 2) by A57, XXREAL_0:2;

then p + ((min (r,(g - p))) / 2) in { s where s is Real : ( p - r < s & s < p + r ) } by A52;

then p + ((min (r,(g - p))) / 2) in ].(p - r),(p + r).[ by RCOMP_1:def 2;

then [.(p - ((min (r,(g - p))) / 2)),(p + ((min (r,(g - p))) / 2)).] c= N1 by A48, A55, XXREAL_2:def 12;

hence (f | X) . x in N1 by A66; :: thesis: verum

suppose A67:
(f | X) . x0 = g
; :: thesis: ex N being Neighbourhood of x0 st

for x being Real st x in dom (f | X) & x in N holds

(f | X) . x in N1

for x being Real st x in dom (f | X) & x in N holds

(f | X) . x in N1

A68:
].p,g.[ c= [.p,g.]
by XXREAL_1:25;

consider r being Real such that

A69: r > 0 and

A70: N1 = ].(g - r),(g + r).[ by A67, RCOMP_1:def 6;

reconsider r = r as Real ;

set R = (min (r,(g - p))) / 2;

g - p > 0 by A4, XREAL_1:50;

then A71: min (r,(g - p)) > 0 by A69, XXREAL_0:15;

then A72: (min (r,(g - p))) / 2 < min (r,(g - p)) by XREAL_1:216;

A73: g - ((min (r,(g - p))) / 2) < g by A71, XREAL_1:44, XREAL_1:215;

min (r,(g - p)) <= g - p by XXREAL_0:17;

then (min (r,(g - p))) / 2 < g - p by A72, XXREAL_0:2;

then ((min (r,(g - p))) / 2) + p < g by XREAL_1:20;

then g - ((min (r,(g - p))) / 2) > p by XREAL_1:20;

then g - ((min (r,(g - p))) / 2) in { s where s is Real : ( p < s & s < g ) } by A73;

then g - ((min (r,(g - p))) / 2) in ].p,g.[ by RCOMP_1:def 2;

then consider x1 being Element of REAL such that

A74: ( x1 in dom (f | X) & x1 in X ) and

A75: g - ((min (r,(g - p))) / 2) = (f | X) . x1 by A3, A7, A68, PARTFUN2:59;

then A78: (min (r,(g - p))) / 2 < r by A72, XXREAL_0:2;

then A79: g + ((min (r,(g - p))) / 2) < g + r by XREAL_1:6;

- r < - ((min (r,(g - p))) / 2) by A78, XREAL_1:24;

then A80: g + (- r) < g + (- ((min (r,(g - p))) / 2)) by XREAL_1:6;

g < g + r by A69, XREAL_1:29;

then g - ((min (r,(g - p))) / 2) < g + r by A73, XXREAL_0:2;

then g - ((min (r,(g - p))) / 2) in { s where s is Real : ( g - r < s & s < g + r ) } by A80;

then A81: g - ((min (r,(g - p))) / 2) in ].(g - r),(g + r).[ by RCOMP_1:def 2;

A82: x1 in X /\ (dom (f | X)) by A74, XBOOLE_0:def 4;

A83: g < g + ((min (r,(g - p))) / 2) by A71, XREAL_1:29, XREAL_1:215;

x1 <> x0 by A67, A71, A75, XREAL_1:44, XREAL_1:215;

then x1 < x0 by A76, XXREAL_0:1;

then reconsider N = ].(x0 - (x0 - x1)),(x0 + (x0 - x1)).[ as Neighbourhood of x0 by RCOMP_1:def 6, XREAL_1:50;

take N = N; :: thesis: for x being Real st x in dom (f | X) & x in N holds

(f | X) . x in N1

let x be Real; :: thesis: ( x in dom (f | X) & x in N implies (f | X) . x in N1 )

assume that

A84: x in dom (f | X) and

A85: x in N ; :: thesis: (f | X) . x in N1

x in { s where s is Real : ( x0 - (x0 - x1) < s & s < x0 + (x0 - x1) ) } by A85, RCOMP_1:def 2;

then A86: ex s being Real st

( s = x & x0 - (x0 - x1) < s & s < x0 + (x0 - x1) ) ;

(f | X) . x in [.p,g.] by A3, A7, A84, FUNCT_1:def 6;

then (f | X) . x in { s where s is Real : ( p <= s & s <= g ) } by RCOMP_1:def 1;

then ex s being Real st

( s = (f | X) . x & p <= s & s <= g ) ;

then A87: (f | X) . x <= g + ((min (r,(g - p))) / 2) by A83, XXREAL_0:2;

x in X /\ (dom (f | X)) by A84, XBOOLE_0:def 4;

then g - ((min (r,(g - p))) / 2) <= (f | X) . x by A5, A75, A82, A86, RFUNCT_2:22;

then (f | X) . x in { s where s is Real : ( g - ((min (r,(g - p))) / 2) <= s & s <= g + ((min (r,(g - p))) / 2) ) } by A87;

then A88: (f | X) . x in [.(g - ((min (r,(g - p))) / 2)),(g + ((min (r,(g - p))) / 2)).] by RCOMP_1:def 1;

g - r < g by A69, XREAL_1:44;

then g - r < g + ((min (r,(g - p))) / 2) by A83, XXREAL_0:2;

then g + ((min (r,(g - p))) / 2) in { s where s is Real : ( g - r < s & s < g + r ) } by A79;

then g + ((min (r,(g - p))) / 2) in ].(g - r),(g + r).[ by RCOMP_1:def 2;

then [.(g - ((min (r,(g - p))) / 2)),(g + ((min (r,(g - p))) / 2)).] c= N1 by A70, A81, XXREAL_2:def 12;

hence (f | X) . x in N1 by A88; :: thesis: verum

end;consider r being Real such that

A69: r > 0 and

A70: N1 = ].(g - r),(g + r).[ by A67, RCOMP_1:def 6;

reconsider r = r as Real ;

set R = (min (r,(g - p))) / 2;

g - p > 0 by A4, XREAL_1:50;

then A71: min (r,(g - p)) > 0 by A69, XXREAL_0:15;

then A72: (min (r,(g - p))) / 2 < min (r,(g - p)) by XREAL_1:216;

A73: g - ((min (r,(g - p))) / 2) < g by A71, XREAL_1:44, XREAL_1:215;

min (r,(g - p)) <= g - p by XXREAL_0:17;

then (min (r,(g - p))) / 2 < g - p by A72, XXREAL_0:2;

then ((min (r,(g - p))) / 2) + p < g by XREAL_1:20;

then g - ((min (r,(g - p))) / 2) > p by XREAL_1:20;

then g - ((min (r,(g - p))) / 2) in { s where s is Real : ( p < s & s < g ) } by A73;

then g - ((min (r,(g - p))) / 2) in ].p,g.[ by RCOMP_1:def 2;

then consider x1 being Element of REAL such that

A74: ( x1 in dom (f | X) & x1 in X ) and

A75: g - ((min (r,(g - p))) / 2) = (f | X) . x1 by A3, A7, A68, PARTFUN2:59;

A76: now :: thesis: not x0 < x1

min (r,(g - p)) <= r
by XXREAL_0:17;assume A77:
x0 < x1
; :: thesis: contradiction

( x0 in X /\ (dom (f | X)) & x1 in X /\ (dom (f | X)) ) by A8, A74, XBOOLE_0:def 4;

hence contradiction by A5, A67, A73, A75, A77, RFUNCT_2:22; :: thesis: verum

end;( x0 in X /\ (dom (f | X)) & x1 in X /\ (dom (f | X)) ) by A8, A74, XBOOLE_0:def 4;

hence contradiction by A5, A67, A73, A75, A77, RFUNCT_2:22; :: thesis: verum

then A78: (min (r,(g - p))) / 2 < r by A72, XXREAL_0:2;

then A79: g + ((min (r,(g - p))) / 2) < g + r by XREAL_1:6;

- r < - ((min (r,(g - p))) / 2) by A78, XREAL_1:24;

then A80: g + (- r) < g + (- ((min (r,(g - p))) / 2)) by XREAL_1:6;

g < g + r by A69, XREAL_1:29;

then g - ((min (r,(g - p))) / 2) < g + r by A73, XXREAL_0:2;

then g - ((min (r,(g - p))) / 2) in { s where s is Real : ( g - r < s & s < g + r ) } by A80;

then A81: g - ((min (r,(g - p))) / 2) in ].(g - r),(g + r).[ by RCOMP_1:def 2;

A82: x1 in X /\ (dom (f | X)) by A74, XBOOLE_0:def 4;

A83: g < g + ((min (r,(g - p))) / 2) by A71, XREAL_1:29, XREAL_1:215;

x1 <> x0 by A67, A71, A75, XREAL_1:44, XREAL_1:215;

then x1 < x0 by A76, XXREAL_0:1;

then reconsider N = ].(x0 - (x0 - x1)),(x0 + (x0 - x1)).[ as Neighbourhood of x0 by RCOMP_1:def 6, XREAL_1:50;

take N = N; :: thesis: for x being Real st x in dom (f | X) & x in N holds

(f | X) . x in N1

let x be Real; :: thesis: ( x in dom (f | X) & x in N implies (f | X) . x in N1 )

assume that

A84: x in dom (f | X) and

A85: x in N ; :: thesis: (f | X) . x in N1

x in { s where s is Real : ( x0 - (x0 - x1) < s & s < x0 + (x0 - x1) ) } by A85, RCOMP_1:def 2;

then A86: ex s being Real st

( s = x & x0 - (x0 - x1) < s & s < x0 + (x0 - x1) ) ;

(f | X) . x in [.p,g.] by A3, A7, A84, FUNCT_1:def 6;

then (f | X) . x in { s where s is Real : ( p <= s & s <= g ) } by RCOMP_1:def 1;

then ex s being Real st

( s = (f | X) . x & p <= s & s <= g ) ;

then A87: (f | X) . x <= g + ((min (r,(g - p))) / 2) by A83, XXREAL_0:2;

x in X /\ (dom (f | X)) by A84, XBOOLE_0:def 4;

then g - ((min (r,(g - p))) / 2) <= (f | X) . x by A5, A75, A82, A86, RFUNCT_2:22;

then (f | X) . x in { s where s is Real : ( g - ((min (r,(g - p))) / 2) <= s & s <= g + ((min (r,(g - p))) / 2) ) } by A87;

then A88: (f | X) . x in [.(g - ((min (r,(g - p))) / 2)),(g + ((min (r,(g - p))) / 2)).] by RCOMP_1:def 1;

g - r < g by A69, XREAL_1:44;

then g - r < g + ((min (r,(g - p))) / 2) by A83, XXREAL_0:2;

then g + ((min (r,(g - p))) / 2) in { s where s is Real : ( g - r < s & s < g + r ) } by A79;

then g + ((min (r,(g - p))) / 2) in ].(g - r),(g + r).[ by RCOMP_1:def 2;

then [.(g - ((min (r,(g - p))) / 2)),(g + ((min (r,(g - p))) / 2)).] c= N1 by A70, A81, XXREAL_2:def 12;

hence (f | X) . x in N1 by A88; :: thesis: verum

A89: for x1 being Real st x1 in dom (f | X) & x1 in N holds

(f | X) . x1 in N1 ;

take N = N; :: thesis: for x1 being Real st x1 in dom (f | X) & x1 in N holds

(f | X) . x1 in N1

thus for x1 being Real st x1 in dom (f | X) & x1 in N holds

(f | X) . x1 in N1 by A89; :: thesis: verum

suppose
f | X is non-increasing
; :: thesis: f | X is continuous

then A90:
(f | X) | X is non-increasing
;

for x0 being Real st x0 in dom (f | X) holds

f | X is_continuous_in x0

end;for x0 being Real st x0 in dom (f | X) holds

f | X is_continuous_in x0

proof

hence
f | X is continuous
; :: thesis: verum
A91:
[.p,g.] = ].p,g.[ \/ {p,g}
by A2, XXREAL_1:128;

let x0 be Real; :: thesis: ( x0 in dom (f | X) implies f | X is_continuous_in x0 )

A92: (f | X) .: X = f .: X by RELAT_1:129;

assume A93: x0 in dom (f | X) ; :: thesis: f | X is_continuous_in x0

A94: (f | X) . x0 in (f | X) .: X by A93, FUNCT_1:def 6;

reconsider x0 = x0 as Real ;

(f | X) . x0 in [.p,g.] by A3, A94, RELAT_1:129;

then A95: ( (f | X) . x0 in ].p,g.[ or (f | X) . x0 in {p,g} ) by A91, XBOOLE_0:def 3;

end;let x0 be Real; :: thesis: ( x0 in dom (f | X) implies f | X is_continuous_in x0 )

A92: (f | X) .: X = f .: X by RELAT_1:129;

assume A93: x0 in dom (f | X) ; :: thesis: f | X is_continuous_in x0

A94: (f | X) . x0 in (f | X) .: X by A93, FUNCT_1:def 6;

reconsider x0 = x0 as Real ;

(f | X) . x0 in [.p,g.] by A3, A94, RELAT_1:129;

then A95: ( (f | X) . x0 in ].p,g.[ or (f | X) . x0 in {p,g} ) by A91, XBOOLE_0:def 3;

now :: thesis: for N1 being Neighbourhood of (f | X) . x0 ex N being Neighbourhood of x0 st

for x1 being Real st x1 in dom (f | X) & x1 in N holds

(f | X) . x1 in N1

hence
f | X is_continuous_in x0
by Th4; :: thesis: verumfor x1 being Real st x1 in dom (f | X) & x1 in N holds

(f | X) . x1 in N1

let N1 be Neighbourhood of (f | X) . x0; :: thesis: ex N being Neighbourhood of x0 st

for x1 being Real st x1 in dom (f | X) & x1 in N holds

(f | X) . x1 in N1

A174: for x1 being Real st x1 in dom (f | X) & x1 in N holds

(f | X) . x1 in N1 ;

take N = N; :: thesis: for x1 being Real st x1 in dom (f | X) & x1 in N holds

(f | X) . x1 in N1

thus for x1 being Real st x1 in dom (f | X) & x1 in N holds

(f | X) . x1 in N1 by A174; :: thesis: verum

end;for x1 being Real st x1 in dom (f | X) & x1 in N holds

(f | X) . x1 in N1

now :: thesis: ex N being Neighbourhood of x0 st

for x being Real st x in dom (f | X) & x in N holds

(f | X) . x in N1end;

then consider N being Neighbourhood of x0 such that for x being Real st x in dom (f | X) & x in N holds

(f | X) . x in N1

per cases
( (f | X) . x0 in ].p,g.[ or (f | X) . x0 = p or (f | X) . x0 = g )
by A95, TARSKI:def 2;

end;

suppose
(f | X) . x0 in ].p,g.[
; :: thesis: ex N being Neighbourhood of x0 st

for x being Real st x in dom (f | X) & x in N holds

(f | X) . x in N1

for x being Real st x in dom (f | X) & x in N holds

(f | X) . x in N1

then consider N2 being Neighbourhood of (f | X) . x0 such that

A96: N2 c= ].p,g.[ by RCOMP_1:18;

A97: ].p,g.[ c= [.p,g.] by XXREAL_1:25;

consider N3 being Neighbourhood of (f | X) . x0 such that

A98: N3 c= N1 and

A99: N3 c= N2 by RCOMP_1:17;

consider r being Real such that

A100: r > 0 and

A101: N3 = ].(((f | X) . x0) - r),(((f | X) . x0) + r).[ by RCOMP_1:def 6;

reconsider r = r as Real ;

A102: ((f | X) . x0) + (r / 2) < (((f | X) . x0) + (r / 2)) + (r / 2) by A100, XREAL_1:29, XREAL_1:215;

set M2 = ((f | X) . x0) + (r / 2);

A103: (f | X) . x0 < ((f | X) . x0) + (r / 2) by A100, XREAL_1:29, XREAL_1:215;

A104: (f | X) . x0 < ((f | X) . x0) + r by A100, XREAL_1:29;

then ((f | X) . x0) - r < (((f | X) . x0) + r) - r by XREAL_1:9;

then ((f | X) . x0) - r < ((f | X) . x0) + (r / 2) by A103, XXREAL_0:2;

then ((f | X) . x0) + (r / 2) in { s where s is Real : ( ((f | X) . x0) - r < s & s < ((f | X) . x0) + r ) } by A102;

then A105: ((f | X) . x0) + (r / 2) in ].(((f | X) . x0) - r),(((f | X) . x0) + r).[ by RCOMP_1:def 2;

then ((f | X) . x0) + (r / 2) in N2 by A99, A101;

then ((f | X) . x0) + (r / 2) in ].p,g.[ by A96;

then consider x2 being Element of REAL such that

A106: ( x2 in dom (f | X) & x2 in X ) and

A107: ((f | X) . x0) + (r / 2) = (f | X) . x2 by A3, A92, A97, PARTFUN2:59;

A108: ].p,g.[ c= [.p,g.] by XXREAL_1:25;

set M1 = ((f | X) . x0) - (r / 2);

A109: ((f | X) . x0) - r < (((f | X) . x0) - r) + (r / 2) by A100, XREAL_1:29, XREAL_1:215;

((f | X) . x0) - (r / 2) < (f | X) . x0 by A103, XREAL_1:19;

then ((f | X) . x0) - (r / 2) < ((f | X) . x0) + r by A104, XXREAL_0:2;

then ((f | X) . x0) - (r / 2) in { s where s is Real : ( ((f | X) . x0) - r < s & s < ((f | X) . x0) + r ) } by A109;

then A110: ((f | X) . x0) - (r / 2) in ].(((f | X) . x0) - r),(((f | X) . x0) + r).[ by RCOMP_1:def 2;

then ((f | X) . x0) - (r / 2) in N2 by A99, A101;

then ((f | X) . x0) - (r / 2) in ].p,g.[ by A96;

then consider x1 being Element of REAL such that

A111: ( x1 in dom (f | X) & x1 in X ) and

A112: ((f | X) . x0) - (r / 2) = (f | X) . x1 by A3, A92, A108, PARTFUN2:59;

A113: (f | X) . x0 < ((f | X) . x0) + (r / 2) by A100, XREAL_1:29, XREAL_1:215;

then A114: ((f | X) . x0) - (r / 2) < (f | X) . x0 by XREAL_1:19;

then x0 > x2 by A118, XXREAL_0:1;

then A120: x0 - x2 > 0 by XREAL_1:50;

set R = min ((x1 - x0),(x0 - x2));

A121: min ((x1 - x0),(x0 - x2)) <= x1 - x0 by XXREAL_0:17;

x1 <> x0 by A112, A113, XREAL_1:19;

then x1 > x0 by A115, XXREAL_0:1;

then x1 - x0 > 0 by XREAL_1:50;

then min ((x1 - x0),(x0 - x2)) > 0 by A120, XXREAL_0:15;

then reconsider N = ].(x0 - (min ((x1 - x0),(x0 - x2)))),(x0 + (min ((x1 - x0),(x0 - x2)))).[ as Neighbourhood of x0 by RCOMP_1:def 6;

take N = N; :: thesis: for x being Real st x in dom (f | X) & x in N holds

(f | X) . x in N1

let x be Real; :: thesis: ( x in dom (f | X) & x in N implies (f | X) . x in N1 )

assume that

A122: x in dom (f | X) and

A123: x in N ; :: thesis: (f | X) . x in N1

A124: x in X /\ (dom (f | X)) by A122, XBOOLE_1:28;

x in { s where s is Real : ( x0 - (min ((x1 - x0),(x0 - x2))) < s & s < x0 + (min ((x1 - x0),(x0 - x2))) ) } by A123, RCOMP_1:def 2;

then A125: ex s being Real st

( s = x & x0 - (min ((x1 - x0),(x0 - x2))) < s & s < x0 + (min ((x1 - x0),(x0 - x2))) ) ;

then x0 < (min ((x1 - x0),(x0 - x2))) + x by XREAL_1:19;

then A126: x0 - x < ((min ((x1 - x0),(x0 - x2))) + x) - x by XREAL_1:9;

x - x0 < min ((x1 - x0),(x0 - x2)) by A125, XREAL_1:19;

then x - x0 < x1 - x0 by A121, XXREAL_0:2;

then A127: (x - x0) + x0 < (x1 - x0) + x0 by XREAL_1:6;

x1 in X /\ (dom (f | X)) by A111, XBOOLE_0:def 4;

then A128: (f | X) . x1 <= (f | X) . x by A90, A127, A124, RFUNCT_2:23;

min ((x1 - x0),(x0 - x2)) <= x0 - x2 by XXREAL_0:17;

then x0 - x < x0 - x2 by A126, XXREAL_0:2;

then - (x0 - x) > - (x0 - x2) by XREAL_1:24;

then A129: (x - x0) + x0 > (x2 - x0) + x0 by XREAL_1:6;

x2 in X /\ (dom (f | X)) by A106, XBOOLE_0:def 4;

then (f | X) . x <= (f | X) . x2 by A90, A129, A124, RFUNCT_2:23;

then (f | X) . x in { s where s is Real : ( ((f | X) . x0) - (r / 2) <= s & s <= ((f | X) . x0) + (r / 2) ) } by A112, A107, A128;

then A130: (f | X) . x in [.(((f | X) . x0) - (r / 2)),(((f | X) . x0) + (r / 2)).] by RCOMP_1:def 1;

[.(((f | X) . x0) - (r / 2)),(((f | X) . x0) + (r / 2)).] c= ].(((f | X) . x0) - r),(((f | X) . x0) + r).[ by A110, A105, XXREAL_2:def 12;

then (f | X) . x in N3 by A101, A130;

hence (f | X) . x in N1 by A98; :: thesis: verum

end;A96: N2 c= ].p,g.[ by RCOMP_1:18;

A97: ].p,g.[ c= [.p,g.] by XXREAL_1:25;

consider N3 being Neighbourhood of (f | X) . x0 such that

A98: N3 c= N1 and

A99: N3 c= N2 by RCOMP_1:17;

consider r being Real such that

A100: r > 0 and

A101: N3 = ].(((f | X) . x0) - r),(((f | X) . x0) + r).[ by RCOMP_1:def 6;

reconsider r = r as Real ;

A102: ((f | X) . x0) + (r / 2) < (((f | X) . x0) + (r / 2)) + (r / 2) by A100, XREAL_1:29, XREAL_1:215;

set M2 = ((f | X) . x0) + (r / 2);

A103: (f | X) . x0 < ((f | X) . x0) + (r / 2) by A100, XREAL_1:29, XREAL_1:215;

A104: (f | X) . x0 < ((f | X) . x0) + r by A100, XREAL_1:29;

then ((f | X) . x0) - r < (((f | X) . x0) + r) - r by XREAL_1:9;

then ((f | X) . x0) - r < ((f | X) . x0) + (r / 2) by A103, XXREAL_0:2;

then ((f | X) . x0) + (r / 2) in { s where s is Real : ( ((f | X) . x0) - r < s & s < ((f | X) . x0) + r ) } by A102;

then A105: ((f | X) . x0) + (r / 2) in ].(((f | X) . x0) - r),(((f | X) . x0) + r).[ by RCOMP_1:def 2;

then ((f | X) . x0) + (r / 2) in N2 by A99, A101;

then ((f | X) . x0) + (r / 2) in ].p,g.[ by A96;

then consider x2 being Element of REAL such that

A106: ( x2 in dom (f | X) & x2 in X ) and

A107: ((f | X) . x0) + (r / 2) = (f | X) . x2 by A3, A92, A97, PARTFUN2:59;

A108: ].p,g.[ c= [.p,g.] by XXREAL_1:25;

set M1 = ((f | X) . x0) - (r / 2);

A109: ((f | X) . x0) - r < (((f | X) . x0) - r) + (r / 2) by A100, XREAL_1:29, XREAL_1:215;

((f | X) . x0) - (r / 2) < (f | X) . x0 by A103, XREAL_1:19;

then ((f | X) . x0) - (r / 2) < ((f | X) . x0) + r by A104, XXREAL_0:2;

then ((f | X) . x0) - (r / 2) in { s where s is Real : ( ((f | X) . x0) - r < s & s < ((f | X) . x0) + r ) } by A109;

then A110: ((f | X) . x0) - (r / 2) in ].(((f | X) . x0) - r),(((f | X) . x0) + r).[ by RCOMP_1:def 2;

then ((f | X) . x0) - (r / 2) in N2 by A99, A101;

then ((f | X) . x0) - (r / 2) in ].p,g.[ by A96;

then consider x1 being Element of REAL such that

A111: ( x1 in dom (f | X) & x1 in X ) and

A112: ((f | X) . x0) - (r / 2) = (f | X) . x1 by A3, A92, A108, PARTFUN2:59;

A113: (f | X) . x0 < ((f | X) . x0) + (r / 2) by A100, XREAL_1:29, XREAL_1:215;

then A114: ((f | X) . x0) - (r / 2) < (f | X) . x0 by XREAL_1:19;

A115: now :: thesis: not x0 > x1

A117:
((f | X) . x0) + (r / 2) > (f | X) . x0
by A100, XREAL_1:29, XREAL_1:215;assume A116:
x0 > x1
; :: thesis: contradiction

( x0 in X /\ (dom (f | X)) & x1 in X /\ (dom (f | X)) ) by A93, A111, XBOOLE_0:def 4;

hence contradiction by A90, A112, A114, A116, RFUNCT_2:23; :: thesis: verum

end;( x0 in X /\ (dom (f | X)) & x1 in X /\ (dom (f | X)) ) by A93, A111, XBOOLE_0:def 4;

hence contradiction by A90, A112, A114, A116, RFUNCT_2:23; :: thesis: verum

A118: now :: thesis: not x2 > x0

x0 <> x2
by A100, A107, XREAL_1:29, XREAL_1:215;assume A119:
x2 > x0
; :: thesis: contradiction

( x0 in X /\ (dom (f | X)) & x2 in X /\ (dom (f | X)) ) by A93, A106, XBOOLE_0:def 4;

hence contradiction by A90, A107, A117, A119, RFUNCT_2:23; :: thesis: verum

end;( x0 in X /\ (dom (f | X)) & x2 in X /\ (dom (f | X)) ) by A93, A106, XBOOLE_0:def 4;

hence contradiction by A90, A107, A117, A119, RFUNCT_2:23; :: thesis: verum

then x0 > x2 by A118, XXREAL_0:1;

then A120: x0 - x2 > 0 by XREAL_1:50;

set R = min ((x1 - x0),(x0 - x2));

A121: min ((x1 - x0),(x0 - x2)) <= x1 - x0 by XXREAL_0:17;

x1 <> x0 by A112, A113, XREAL_1:19;

then x1 > x0 by A115, XXREAL_0:1;

then x1 - x0 > 0 by XREAL_1:50;

then min ((x1 - x0),(x0 - x2)) > 0 by A120, XXREAL_0:15;

then reconsider N = ].(x0 - (min ((x1 - x0),(x0 - x2)))),(x0 + (min ((x1 - x0),(x0 - x2)))).[ as Neighbourhood of x0 by RCOMP_1:def 6;

take N = N; :: thesis: for x being Real st x in dom (f | X) & x in N holds

(f | X) . x in N1

let x be Real; :: thesis: ( x in dom (f | X) & x in N implies (f | X) . x in N1 )

assume that

A122: x in dom (f | X) and

A123: x in N ; :: thesis: (f | X) . x in N1

A124: x in X /\ (dom (f | X)) by A122, XBOOLE_1:28;

x in { s where s is Real : ( x0 - (min ((x1 - x0),(x0 - x2))) < s & s < x0 + (min ((x1 - x0),(x0 - x2))) ) } by A123, RCOMP_1:def 2;

then A125: ex s being Real st

( s = x & x0 - (min ((x1 - x0),(x0 - x2))) < s & s < x0 + (min ((x1 - x0),(x0 - x2))) ) ;

then x0 < (min ((x1 - x0),(x0 - x2))) + x by XREAL_1:19;

then A126: x0 - x < ((min ((x1 - x0),(x0 - x2))) + x) - x by XREAL_1:9;

x - x0 < min ((x1 - x0),(x0 - x2)) by A125, XREAL_1:19;

then x - x0 < x1 - x0 by A121, XXREAL_0:2;

then A127: (x - x0) + x0 < (x1 - x0) + x0 by XREAL_1:6;

x1 in X /\ (dom (f | X)) by A111, XBOOLE_0:def 4;

then A128: (f | X) . x1 <= (f | X) . x by A90, A127, A124, RFUNCT_2:23;

min ((x1 - x0),(x0 - x2)) <= x0 - x2 by XXREAL_0:17;

then x0 - x < x0 - x2 by A126, XXREAL_0:2;

then - (x0 - x) > - (x0 - x2) by XREAL_1:24;

then A129: (x - x0) + x0 > (x2 - x0) + x0 by XREAL_1:6;

x2 in X /\ (dom (f | X)) by A106, XBOOLE_0:def 4;

then (f | X) . x <= (f | X) . x2 by A90, A129, A124, RFUNCT_2:23;

then (f | X) . x in { s where s is Real : ( ((f | X) . x0) - (r / 2) <= s & s <= ((f | X) . x0) + (r / 2) ) } by A112, A107, A128;

then A130: (f | X) . x in [.(((f | X) . x0) - (r / 2)),(((f | X) . x0) + (r / 2)).] by RCOMP_1:def 1;

[.(((f | X) . x0) - (r / 2)),(((f | X) . x0) + (r / 2)).] c= ].(((f | X) . x0) - r),(((f | X) . x0) + r).[ by A110, A105, XXREAL_2:def 12;

then (f | X) . x in N3 by A101, A130;

hence (f | X) . x in N1 by A98; :: thesis: verum

suppose A131:
(f | X) . x0 = p
; :: thesis: ex N being Neighbourhood of x0 st

for x being Real st x in dom (f | X) & x in N holds

(f | X) . x in N1

for x being Real st x in dom (f | X) & x in N holds

(f | X) . x in N1

then consider r being Real such that

A132: r > 0 and

A133: N1 = ].(p - r),(p + r).[ by RCOMP_1:def 6;

reconsider r = r as Real ;

set R = (min (r,(g - p))) / 2;

g - p > 0 by A4, XREAL_1:50;

then A134: min (r,(g - p)) > 0 by A132, XXREAL_0:15;

then A135: (min (r,(g - p))) / 2 < min (r,(g - p)) by XREAL_1:216;

min (r,(g - p)) <= r by XXREAL_0:17;

then A136: (min (r,(g - p))) / 2 < r by A135, XXREAL_0:2;

then A137: p + ((min (r,(g - p))) / 2) < p + r by XREAL_1:6;

A138: p - ((min (r,(g - p))) / 2) < p by A134, XREAL_1:44, XREAL_1:215;

- r < - ((min (r,(g - p))) / 2) by A136, XREAL_1:24;

then A139: p + (- r) < p + (- ((min (r,(g - p))) / 2)) by XREAL_1:6;

p < p + r by A132, XREAL_1:29;

then p - ((min (r,(g - p))) / 2) < p + r by A138, XXREAL_0:2;

then p - ((min (r,(g - p))) / 2) in { s where s is Real : ( p - r < s & s < p + r ) } by A139;

then A140: p - ((min (r,(g - p))) / 2) in ].(p - r),(p + r).[ by RCOMP_1:def 2;

A141: ].p,g.[ c= [.p,g.] by XXREAL_1:25;

A142: p < p + ((min (r,(g - p))) / 2) by A134, XREAL_1:29, XREAL_1:215;

min (r,(g - p)) <= g - p by XXREAL_0:17;

then (min (r,(g - p))) / 2 < g - p by A135, XXREAL_0:2;

then p + ((min (r,(g - p))) / 2) < g by XREAL_1:20;

then p + ((min (r,(g - p))) / 2) in { s where s is Real : ( p < s & s < g ) } by A142;

then p + ((min (r,(g - p))) / 2) in ].p,g.[ by RCOMP_1:def 2;

then consider x1 being Element of REAL such that

A143: ( x1 in dom (f | X) & x1 in X ) and

A144: p + ((min (r,(g - p))) / 2) = (f | X) . x1 by A3, A92, A141, PARTFUN2:59;

A145: x1 in X /\ (dom (f | X)) by A143, XBOOLE_0:def 4;

then reconsider N = ].(x0 - (x0 - x1)),(x0 + (x0 - x1)).[ as Neighbourhood of x0 by RCOMP_1:def 6, XREAL_1:50;

take N = N; :: thesis: for x being Real st x in dom (f | X) & x in N holds

(f | X) . x in N1

let x be Real; :: thesis: ( x in dom (f | X) & x in N implies (f | X) . x in N1 )

assume that

A147: x in dom (f | X) and

A148: x in N ; :: thesis: (f | X) . x in N1

x in { s where s is Real : ( x0 - (x0 - x1) < s & s < x0 + (x0 - x1) ) } by A148, RCOMP_1:def 2;

then A149: ex s being Real st

( s = x & x0 - (x0 - x1) < s & s < x0 + (x0 - x1) ) ;

(f | X) . x in [.p,g.] by A3, A92, A147, FUNCT_1:def 6;

then (f | X) . x in { s where s is Real : ( p <= s & s <= g ) } by RCOMP_1:def 1;

then ex s being Real st

( s = (f | X) . x & p <= s & s <= g ) ;

then A150: p - ((min (r,(g - p))) / 2) <= (f | X) . x by A138, XXREAL_0:2;

x in X /\ (dom (f | X)) by A147, XBOOLE_0:def 4;

then (f | X) . x <= p + ((min (r,(g - p))) / 2) by A90, A144, A145, A149, RFUNCT_2:23;

then (f | X) . x in { s where s is Real : ( p - ((min (r,(g - p))) / 2) <= s & s <= p + ((min (r,(g - p))) / 2) ) } by A150;

then A151: (f | X) . x in [.(p - ((min (r,(g - p))) / 2)),(p + ((min (r,(g - p))) / 2)).] by RCOMP_1:def 1;

p - r < p by A132, XREAL_1:44;

then p - r < p + ((min (r,(g - p))) / 2) by A142, XXREAL_0:2;

then p + ((min (r,(g - p))) / 2) in { s where s is Real : ( p - r < s & s < p + r ) } by A137;

then p + ((min (r,(g - p))) / 2) in ].(p - r),(p + r).[ by RCOMP_1:def 2;

then [.(p - ((min (r,(g - p))) / 2)),(p + ((min (r,(g - p))) / 2)).] c= N1 by A133, A140, XXREAL_2:def 12;

hence (f | X) . x in N1 by A151; :: thesis: verum

end;A132: r > 0 and

A133: N1 = ].(p - r),(p + r).[ by RCOMP_1:def 6;

reconsider r = r as Real ;

set R = (min (r,(g - p))) / 2;

g - p > 0 by A4, XREAL_1:50;

then A134: min (r,(g - p)) > 0 by A132, XXREAL_0:15;

then A135: (min (r,(g - p))) / 2 < min (r,(g - p)) by XREAL_1:216;

min (r,(g - p)) <= r by XXREAL_0:17;

then A136: (min (r,(g - p))) / 2 < r by A135, XXREAL_0:2;

then A137: p + ((min (r,(g - p))) / 2) < p + r by XREAL_1:6;

A138: p - ((min (r,(g - p))) / 2) < p by A134, XREAL_1:44, XREAL_1:215;

- r < - ((min (r,(g - p))) / 2) by A136, XREAL_1:24;

then A139: p + (- r) < p + (- ((min (r,(g - p))) / 2)) by XREAL_1:6;

p < p + r by A132, XREAL_1:29;

then p - ((min (r,(g - p))) / 2) < p + r by A138, XXREAL_0:2;

then p - ((min (r,(g - p))) / 2) in { s where s is Real : ( p - r < s & s < p + r ) } by A139;

then A140: p - ((min (r,(g - p))) / 2) in ].(p - r),(p + r).[ by RCOMP_1:def 2;

A141: ].p,g.[ c= [.p,g.] by XXREAL_1:25;

A142: p < p + ((min (r,(g - p))) / 2) by A134, XREAL_1:29, XREAL_1:215;

min (r,(g - p)) <= g - p by XXREAL_0:17;

then (min (r,(g - p))) / 2 < g - p by A135, XXREAL_0:2;

then p + ((min (r,(g - p))) / 2) < g by XREAL_1:20;

then p + ((min (r,(g - p))) / 2) in { s where s is Real : ( p < s & s < g ) } by A142;

then p + ((min (r,(g - p))) / 2) in ].p,g.[ by RCOMP_1:def 2;

then consider x1 being Element of REAL such that

A143: ( x1 in dom (f | X) & x1 in X ) and

A144: p + ((min (r,(g - p))) / 2) = (f | X) . x1 by A3, A92, A141, PARTFUN2:59;

A145: x1 in X /\ (dom (f | X)) by A143, XBOOLE_0:def 4;

now :: thesis: not x1 > x0

then
x0 > x1
by A131, A142, A144, XXREAL_0:1;assume A146:
x1 > x0
; :: thesis: contradiction

( x0 in X /\ (dom (f | X)) & x1 in X /\ (dom (f | X)) ) by A93, A143, XBOOLE_0:def 4;

hence contradiction by A90, A131, A142, A144, A146, RFUNCT_2:23; :: thesis: verum

end;( x0 in X /\ (dom (f | X)) & x1 in X /\ (dom (f | X)) ) by A93, A143, XBOOLE_0:def 4;

hence contradiction by A90, A131, A142, A144, A146, RFUNCT_2:23; :: thesis: verum

then reconsider N = ].(x0 - (x0 - x1)),(x0 + (x0 - x1)).[ as Neighbourhood of x0 by RCOMP_1:def 6, XREAL_1:50;

take N = N; :: thesis: for x being Real st x in dom (f | X) & x in N holds

(f | X) . x in N1

let x be Real; :: thesis: ( x in dom (f | X) & x in N implies (f | X) . x in N1 )

assume that

A147: x in dom (f | X) and

A148: x in N ; :: thesis: (f | X) . x in N1

x in { s where s is Real : ( x0 - (x0 - x1) < s & s < x0 + (x0 - x1) ) } by A148, RCOMP_1:def 2;

then A149: ex s being Real st

( s = x & x0 - (x0 - x1) < s & s < x0 + (x0 - x1) ) ;

(f | X) . x in [.p,g.] by A3, A92, A147, FUNCT_1:def 6;

then (f | X) . x in { s where s is Real : ( p <= s & s <= g ) } by RCOMP_1:def 1;

then ex s being Real st

( s = (f | X) . x & p <= s & s <= g ) ;

then A150: p - ((min (r,(g - p))) / 2) <= (f | X) . x by A138, XXREAL_0:2;

x in X /\ (dom (f | X)) by A147, XBOOLE_0:def 4;

then (f | X) . x <= p + ((min (r,(g - p))) / 2) by A90, A144, A145, A149, RFUNCT_2:23;

then (f | X) . x in { s where s is Real : ( p - ((min (r,(g - p))) / 2) <= s & s <= p + ((min (r,(g - p))) / 2) ) } by A150;

then A151: (f | X) . x in [.(p - ((min (r,(g - p))) / 2)),(p + ((min (r,(g - p))) / 2)).] by RCOMP_1:def 1;

p - r < p by A132, XREAL_1:44;

then p - r < p + ((min (r,(g - p))) / 2) by A142, XXREAL_0:2;

then p + ((min (r,(g - p))) / 2) in { s where s is Real : ( p - r < s & s < p + r ) } by A137;

then p + ((min (r,(g - p))) / 2) in ].(p - r),(p + r).[ by RCOMP_1:def 2;

then [.(p - ((min (r,(g - p))) / 2)),(p + ((min (r,(g - p))) / 2)).] c= N1 by A133, A140, XXREAL_2:def 12;

hence (f | X) . x in N1 by A151; :: thesis: verum

suppose A152:
(f | X) . x0 = g
; :: thesis: ex N being Neighbourhood of x0 st

for x being Real st x in dom (f | X) & x in N holds

(f | X) . x in N1

for x being Real st x in dom (f | X) & x in N holds

(f | X) . x in N1

A153:
].p,g.[ c= [.p,g.]
by XXREAL_1:25;

consider r being Real such that

A154: r > 0 and

A155: N1 = ].(g - r),(g + r).[ by A152, RCOMP_1:def 6;

reconsider r = r as Real ;

set R = (min (r,(g - p))) / 2;

g - p > 0 by A4, XREAL_1:50;

then A156: min (r,(g - p)) > 0 by A154, XXREAL_0:15;

then A157: (min (r,(g - p))) / 2 < min (r,(g - p)) by XREAL_1:216;

A158: g - ((min (r,(g - p))) / 2) < g by A156, XREAL_1:44, XREAL_1:215;

min (r,(g - p)) <= g - p by XXREAL_0:17;

then (min (r,(g - p))) / 2 < g - p by A157, XXREAL_0:2;

then ((min (r,(g - p))) / 2) + p < g by XREAL_1:20;

then g - ((min (r,(g - p))) / 2) > p by XREAL_1:20;

then g - ((min (r,(g - p))) / 2) in { s where s is Real : ( p < s & s < g ) } by A158;

then g - ((min (r,(g - p))) / 2) in ].p,g.[ by RCOMP_1:def 2;

then consider x1 being Element of REAL such that

A159: ( x1 in dom (f | X) & x1 in X ) and

A160: g - ((min (r,(g - p))) / 2) = (f | X) . x1 by A3, A92, A153, PARTFUN2:59;

then A163: (min (r,(g - p))) / 2 < r by A157, XXREAL_0:2;

then A164: g + ((min (r,(g - p))) / 2) < g + r by XREAL_1:6;

- r < - ((min (r,(g - p))) / 2) by A163, XREAL_1:24;

then A165: g + (- r) < g + (- ((min (r,(g - p))) / 2)) by XREAL_1:6;

g < g + r by A154, XREAL_1:29;

then g - ((min (r,(g - p))) / 2) < g + r by A158, XXREAL_0:2;

then g - ((min (r,(g - p))) / 2) in { s where s is Real : ( g - r < s & s < g + r ) } by A165;

then A166: g - ((min (r,(g - p))) / 2) in ].(g - r),(g + r).[ by RCOMP_1:def 2;

A167: x1 in X /\ (dom (f | X)) by A159, XBOOLE_0:def 4;

A168: g < g + ((min (r,(g - p))) / 2) by A156, XREAL_1:29, XREAL_1:215;

x1 <> x0 by A152, A156, A160, XREAL_1:44, XREAL_1:215;

then x1 > x0 by A161, XXREAL_0:1;

then reconsider N = ].(x0 - (x1 - x0)),(x0 + (x1 - x0)).[ as Neighbourhood of x0 by RCOMP_1:def 6, XREAL_1:50;

take N = N; :: thesis: for x being Real st x in dom (f | X) & x in N holds

(f | X) . x in N1

let x be Real; :: thesis: ( x in dom (f | X) & x in N implies (f | X) . x in N1 )

assume that

A169: x in dom (f | X) and

A170: x in N ; :: thesis: (f | X) . x in N1

x in { s where s is Real : ( x0 - (x1 - x0) < s & s < x0 + (x1 - x0) ) } by A170, RCOMP_1:def 2;

then A171: ex s being Real st

( s = x & x0 - (x1 - x0) < s & s < x0 + (x1 - x0) ) ;

(f | X) . x in [.p,g.] by A3, A92, A169, FUNCT_1:def 6;

then (f | X) . x in { s where s is Real : ( p <= s & s <= g ) } by RCOMP_1:def 1;

then ex s being Real st

( s = (f | X) . x & p <= s & s <= g ) ;

then A172: (f | X) . x <= g + ((min (r,(g - p))) / 2) by A168, XXREAL_0:2;

x in X /\ (dom (f | X)) by A169, XBOOLE_0:def 4;

then g - ((min (r,(g - p))) / 2) <= (f | X) . x by A90, A160, A167, A171, RFUNCT_2:23;

then (f | X) . x in { s where s is Real : ( g - ((min (r,(g - p))) / 2) <= s & s <= g + ((min (r,(g - p))) / 2) ) } by A172;

then A173: (f | X) . x in [.(g - ((min (r,(g - p))) / 2)),(g + ((min (r,(g - p))) / 2)).] by RCOMP_1:def 1;

g - r < g by A154, XREAL_1:44;

then g - r < g + ((min (r,(g - p))) / 2) by A168, XXREAL_0:2;

then g + ((min (r,(g - p))) / 2) in { s where s is Real : ( g - r < s & s < g + r ) } by A164;

then g + ((min (r,(g - p))) / 2) in ].(g - r),(g + r).[ by RCOMP_1:def 2;

then [.(g - ((min (r,(g - p))) / 2)),(g + ((min (r,(g - p))) / 2)).] c= N1 by A155, A166, XXREAL_2:def 12;

hence (f | X) . x in N1 by A173; :: thesis: verum

end;consider r being Real such that

A154: r > 0 and

A155: N1 = ].(g - r),(g + r).[ by A152, RCOMP_1:def 6;

reconsider r = r as Real ;

set R = (min (r,(g - p))) / 2;

g - p > 0 by A4, XREAL_1:50;

then A156: min (r,(g - p)) > 0 by A154, XXREAL_0:15;

then A157: (min (r,(g - p))) / 2 < min (r,(g - p)) by XREAL_1:216;

A158: g - ((min (r,(g - p))) / 2) < g by A156, XREAL_1:44, XREAL_1:215;

min (r,(g - p)) <= g - p by XXREAL_0:17;

then (min (r,(g - p))) / 2 < g - p by A157, XXREAL_0:2;

then ((min (r,(g - p))) / 2) + p < g by XREAL_1:20;

then g - ((min (r,(g - p))) / 2) > p by XREAL_1:20;

then g - ((min (r,(g - p))) / 2) in { s where s is Real : ( p < s & s < g ) } by A158;

then g - ((min (r,(g - p))) / 2) in ].p,g.[ by RCOMP_1:def 2;

then consider x1 being Element of REAL such that

A159: ( x1 in dom (f | X) & x1 in X ) and

A160: g - ((min (r,(g - p))) / 2) = (f | X) . x1 by A3, A92, A153, PARTFUN2:59;

A161: now :: thesis: not x0 > x1

min (r,(g - p)) <= r
by XXREAL_0:17;assume A162:
x0 > x1
; :: thesis: contradiction

( x0 in X /\ (dom (f | X)) & x1 in X /\ (dom (f | X)) ) by A93, A159, XBOOLE_0:def 4;

hence contradiction by A90, A152, A158, A160, A162, RFUNCT_2:23; :: thesis: verum

end;( x0 in X /\ (dom (f | X)) & x1 in X /\ (dom (f | X)) ) by A93, A159, XBOOLE_0:def 4;

hence contradiction by A90, A152, A158, A160, A162, RFUNCT_2:23; :: thesis: verum

then A163: (min (r,(g - p))) / 2 < r by A157, XXREAL_0:2;

then A164: g + ((min (r,(g - p))) / 2) < g + r by XREAL_1:6;

- r < - ((min (r,(g - p))) / 2) by A163, XREAL_1:24;

then A165: g + (- r) < g + (- ((min (r,(g - p))) / 2)) by XREAL_1:6;

g < g + r by A154, XREAL_1:29;

then g - ((min (r,(g - p))) / 2) < g + r by A158, XXREAL_0:2;

then g - ((min (r,(g - p))) / 2) in { s where s is Real : ( g - r < s & s < g + r ) } by A165;

then A166: g - ((min (r,(g - p))) / 2) in ].(g - r),(g + r).[ by RCOMP_1:def 2;

A167: x1 in X /\ (dom (f | X)) by A159, XBOOLE_0:def 4;

A168: g < g + ((min (r,(g - p))) / 2) by A156, XREAL_1:29, XREAL_1:215;

x1 <> x0 by A152, A156, A160, XREAL_1:44, XREAL_1:215;

then x1 > x0 by A161, XXREAL_0:1;

then reconsider N = ].(x0 - (x1 - x0)),(x0 + (x1 - x0)).[ as Neighbourhood of x0 by RCOMP_1:def 6, XREAL_1:50;

take N = N; :: thesis: for x being Real st x in dom (f | X) & x in N holds

(f | X) . x in N1

let x be Real; :: thesis: ( x in dom (f | X) & x in N implies (f | X) . x in N1 )

assume that

A169: x in dom (f | X) and

A170: x in N ; :: thesis: (f | X) . x in N1

x in { s where s is Real : ( x0 - (x1 - x0) < s & s < x0 + (x1 - x0) ) } by A170, RCOMP_1:def 2;

then A171: ex s being Real st

( s = x & x0 - (x1 - x0) < s & s < x0 + (x1 - x0) ) ;

(f | X) . x in [.p,g.] by A3, A92, A169, FUNCT_1:def 6;

then (f | X) . x in { s where s is Real : ( p <= s & s <= g ) } by RCOMP_1:def 1;

then ex s being Real st

( s = (f | X) . x & p <= s & s <= g ) ;

then A172: (f | X) . x <= g + ((min (r,(g - p))) / 2) by A168, XXREAL_0:2;

x in X /\ (dom (f | X)) by A169, XBOOLE_0:def 4;

then g - ((min (r,(g - p))) / 2) <= (f | X) . x by A90, A160, A167, A171, RFUNCT_2:23;

then (f | X) . x in { s where s is Real : ( g - ((min (r,(g - p))) / 2) <= s & s <= g + ((min (r,(g - p))) / 2) ) } by A172;

then A173: (f | X) . x in [.(g - ((min (r,(g - p))) / 2)),(g + ((min (r,(g - p))) / 2)).] by RCOMP_1:def 1;

g - r < g by A154, XREAL_1:44;

then g - r < g + ((min (r,(g - p))) / 2) by A168, XXREAL_0:2;

then g + ((min (r,(g - p))) / 2) in { s where s is Real : ( g - r < s & s < g + r ) } by A164;

then g + ((min (r,(g - p))) / 2) in ].(g - r),(g + r).[ by RCOMP_1:def 2;

then [.(g - ((min (r,(g - p))) / 2)),(g + ((min (r,(g - p))) / 2)).] c= N1 by A155, A166, XXREAL_2:def 12;

hence (f | X) . x in N1 by A173; :: thesis: verum

A174: for x1 being Real st x1 in dom (f | X) & x1 in N holds

(f | X) . x1 in N1 ;

take N = N; :: thesis: for x1 being Real st x1 in dom (f | X) & x1 in N holds

(f | X) . x1 in N1

thus for x1 being Real st x1 in dom (f | X) & x1 in N holds

(f | X) . x1 in N1 by A174; :: thesis: verum