let X be set ; :: thesis: for f being PartFunc of REAL,REAL st X c= dom f & f | X is monotone & f .: X = REAL holds

f | X is continuous

let f be PartFunc of REAL,REAL; :: thesis: ( X c= dom f & f | X is monotone & f .: X = REAL implies f | X is continuous )

assume that

A1: X c= dom f and

A2: f | X is monotone and

A3: f .: X = REAL ; :: thesis: f | X is continuous

f | X is continuous

let f be PartFunc of REAL,REAL; :: thesis: ( X c= dom f & f | X is monotone & f .: X = REAL implies f | X is continuous )

assume that

A1: X c= dom f and

A2: f | X is monotone and

A3: f .: X = REAL ; :: thesis: f | X is continuous

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 A2, RFUNCT_2:def 5;

end;

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

then A4:
(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
by FCONT_1:def 2; :: thesis: verum
let x0 be Real; :: thesis: ( x0 in dom (f | X) implies f | X is_continuous_in x0 )

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

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

then x0 in X ;

then x0 in (dom f) /\ X by A1, XBOOLE_0:def 4;

then A6: x0 in dom (f | X) by RELAT_1:61;

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

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

then x0 in X ;

then x0 in (dom f) /\ X by A1, XBOOLE_0:def 4;

then A6: x0 in dom (f | X) by RELAT_1:61;

now :: thesis: for N1 being Neighbourhood of (f | X) . x0 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

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

(f | X) . x in N1

let N1 be Neighbourhood of (f | X) . x0; :: 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

consider r being Real such that

A7: r > 0 and

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

reconsider r = r as Real ;

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

reconsider M1 = ((f | X) . x0) - (r / 2) as Element of REAL by XREAL_0:def 1;

consider r1 being Element of REAL such that

A10: ( r1 in dom (f | X) & r1 in X ) and

A11: M1 = (f | X) . r1 by A3, A5, PARTFUN2:59;

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

then A13: M1 < (f | X) . x0 by XREAL_1:19;

consider r2 being Element of REAL such that

A16: ( r2 in dom (f | X) & r2 in X ) and

A17: M2 = (f | X) . r2 by A3, A5, PARTFUN2:59;

A18: M2 > (f | X) . x0 by A7, XREAL_1:29, XREAL_1:215;

then x0 < r2 by A19, XXREAL_0:1;

then A21: r2 - x0 > 0 by XREAL_1:50;

set R = min ((x0 - r1),(r2 - x0));

A22: min ((x0 - r1),(r2 - x0)) <= r2 - x0 by XXREAL_0:17;

r1 <> x0 by A11, A12, XREAL_1:19;

then r1 < x0 by A14, XXREAL_0:1;

then x0 - r1 > 0 by XREAL_1:50;

then min ((x0 - r1),(r2 - x0)) > 0 by A21, XXREAL_0:15;

then reconsider N = ].(x0 - (min ((x0 - r1),(r2 - x0)))),(x0 + (min ((x0 - r1),(r2 - 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

A23: x in dom (f | X) and

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

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

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

A27: (f | X) . x0 < ((f | X) . x0) + r by A7, 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 A9, XXREAL_0:2;

then A28: M2 in ].(((f | X) . x0) - r),(((f | X) . x0) + r).[ by A26;

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

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

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

then M1 in ].(((f | X) . x0) - r),(((f | X) . x0) + r).[ by A29;

then A30: [.M1,M2.] c= ].(((f | X) . x0) - r),(((f | X) . x0) + r).[ by A28, XXREAL_2:def 12;

A31: ex s being Real st

( s = x & x0 - (min ((x0 - r1),(r2 - x0))) < s & s < x0 + (min ((x0 - r1),(r2 - x0))) ) by A24;

then x0 < (min ((x0 - r1),(r2 - x0))) + x by XREAL_1:19;

then A32: x0 - x < ((min ((x0 - r1),(r2 - x0))) + x) - x by XREAL_1:9;

min ((x0 - r1),(r2 - x0)) <= x0 - r1 by XXREAL_0:17;

then x0 - x < x0 - r1 by A32, XXREAL_0:2;

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

then A33: (x - x0) + x0 > (r1 - x0) + x0 by XREAL_1:6;

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

then A34: (f | X) . r1 <= (f | X) . x by A4, A33, A25, RFUNCT_2:22;

x - x0 < min ((x0 - r1),(r2 - x0)) by A31, XREAL_1:19;

then x - x0 < r2 - x0 by A22, XXREAL_0:2;

then A35: (x - x0) + x0 < (r2 - x0) + x0 by XREAL_1:6;

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

then (f | X) . x <= (f | X) . r2 by A4, A35, A25, RFUNCT_2:22;

then (f | X) . x in [.M1,M2.] by A11, A17, A34;

hence (f | X) . x in N1 by A8, A30; :: thesis: verum

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

(f | X) . x in N1

consider r being Real such that

A7: r > 0 and

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

reconsider r = r as Real ;

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

reconsider M1 = ((f | X) . x0) - (r / 2) as Element of REAL by XREAL_0:def 1;

consider r1 being Element of REAL such that

A10: ( r1 in dom (f | X) & r1 in X ) and

A11: M1 = (f | X) . r1 by A3, A5, PARTFUN2:59;

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

then A13: M1 < (f | X) . x0 by XREAL_1:19;

A14: now :: thesis: not x0 < r1

reconsider M2 = ((f | X) . x0) + (r / 2) as Element of REAL by XREAL_0:def 1;assume A15:
x0 < r1
; :: thesis: contradiction

( x0 in X /\ (dom (f | X)) & r1 in X /\ (dom (f | X)) ) by A6, A10, XBOOLE_0:def 4;

hence contradiction by A4, A11, A13, A15, RFUNCT_2:22; :: thesis: verum

end;( x0 in X /\ (dom (f | X)) & r1 in X /\ (dom (f | X)) ) by A6, A10, XBOOLE_0:def 4;

hence contradiction by A4, A11, A13, A15, RFUNCT_2:22; :: thesis: verum

consider r2 being Element of REAL such that

A16: ( r2 in dom (f | X) & r2 in X ) and

A17: M2 = (f | X) . r2 by A3, A5, PARTFUN2:59;

A18: M2 > (f | X) . x0 by A7, XREAL_1:29, XREAL_1:215;

A19: now :: thesis: not r2 < x0

x0 <> r2
by A7, A17, XREAL_1:29, XREAL_1:215;assume A20:
r2 < x0
; :: thesis: contradiction

( x0 in X /\ (dom (f | X)) & r2 in X /\ (dom (f | X)) ) by A6, A16, XBOOLE_0:def 4;

hence contradiction by A4, A17, A18, A20, RFUNCT_2:22; :: thesis: verum

end;( x0 in X /\ (dom (f | X)) & r2 in X /\ (dom (f | X)) ) by A6, A16, XBOOLE_0:def 4;

hence contradiction by A4, A17, A18, A20, RFUNCT_2:22; :: thesis: verum

then x0 < r2 by A19, XXREAL_0:1;

then A21: r2 - x0 > 0 by XREAL_1:50;

set R = min ((x0 - r1),(r2 - x0));

A22: min ((x0 - r1),(r2 - x0)) <= r2 - x0 by XXREAL_0:17;

r1 <> x0 by A11, A12, XREAL_1:19;

then r1 < x0 by A14, XXREAL_0:1;

then x0 - r1 > 0 by XREAL_1:50;

then min ((x0 - r1),(r2 - x0)) > 0 by A21, XXREAL_0:15;

then reconsider N = ].(x0 - (min ((x0 - r1),(r2 - x0)))),(x0 + (min ((x0 - r1),(r2 - 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

A23: x in dom (f | X) and

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

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

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

A27: (f | X) . x0 < ((f | X) . x0) + r by A7, 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 A9, XXREAL_0:2;

then A28: M2 in ].(((f | X) . x0) - r),(((f | X) . x0) + r).[ by A26;

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

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

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

then M1 in ].(((f | X) . x0) - r),(((f | X) . x0) + r).[ by A29;

then A30: [.M1,M2.] c= ].(((f | X) . x0) - r),(((f | X) . x0) + r).[ by A28, XXREAL_2:def 12;

A31: ex s being Real st

( s = x & x0 - (min ((x0 - r1),(r2 - x0))) < s & s < x0 + (min ((x0 - r1),(r2 - x0))) ) by A24;

then x0 < (min ((x0 - r1),(r2 - x0))) + x by XREAL_1:19;

then A32: x0 - x < ((min ((x0 - r1),(r2 - x0))) + x) - x by XREAL_1:9;

min ((x0 - r1),(r2 - x0)) <= x0 - r1 by XXREAL_0:17;

then x0 - x < x0 - r1 by A32, XXREAL_0:2;

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

then A33: (x - x0) + x0 > (r1 - x0) + x0 by XREAL_1:6;

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

then A34: (f | X) . r1 <= (f | X) . x by A4, A33, A25, RFUNCT_2:22;

x - x0 < min ((x0 - r1),(r2 - x0)) by A31, XREAL_1:19;

then x - x0 < r2 - x0 by A22, XXREAL_0:2;

then A35: (x - x0) + x0 < (r2 - x0) + x0 by XREAL_1:6;

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

then (f | X) . x <= (f | X) . r2 by A4, A35, A25, RFUNCT_2:22;

then (f | X) . x in [.M1,M2.] by A11, A17, A34;

hence (f | X) . x in N1 by A8, A30; :: thesis: verum

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

then A36:
(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
by FCONT_1:def 2; :: thesis: verum
let x0 be Real; :: thesis: ( x0 in dom (f | X) implies f | X is_continuous_in x0 )

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

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

then x0 in X ;

then x0 in (dom f) /\ X by A1, XBOOLE_0:def 4;

then A38: x0 in dom (f | X) by RELAT_1:61;

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

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

then x0 in X ;

then x0 in (dom f) /\ X by A1, XBOOLE_0:def 4;

then A38: x0 in dom (f | X) by RELAT_1:61;

now :: thesis: for N1 being Neighbourhood of (f | X) . x0 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

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

(f | X) . x in N1

let N1 be Neighbourhood of (f | X) . x0; :: 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

consider r being Real such that

A39: r > 0 and

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

reconsider r = r as Element of REAL by XREAL_0:def 1;

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

reconsider M1 = ((f | X) . x0) - (r / 2) as Element of REAL by XREAL_0:def 1;

consider r1 being Element of REAL such that

A42: ( r1 in dom (f | X) & r1 in X ) and

A43: M1 = (f | X) . r1 by A3, A37, PARTFUN2:59;

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

then A45: M1 < (f | X) . x0 by XREAL_1:19;

consider r2 being Element of REAL such that

A48: ( r2 in dom (f | X) & r2 in X ) and

A49: M2 = (f | X) . r2 by A3, A37, PARTFUN2:59;

A50: M2 > (f | X) . x0 by A39, XREAL_1:29, XREAL_1:215;

then x0 > r2 by A51, XXREAL_0:1;

then A53: x0 - r2 > 0 by XREAL_1:50;

set R = min ((r1 - x0),(x0 - r2));

A54: min ((r1 - x0),(x0 - r2)) <= r1 - x0 by XXREAL_0:17;

r1 <> x0 by A43, A44, XREAL_1:19;

then r1 > x0 by A46, XXREAL_0:1;

then r1 - x0 > 0 by XREAL_1:50;

then min ((r1 - x0),(x0 - r2)) > 0 by A53, XXREAL_0:15;

then reconsider N = ].(x0 - (min ((r1 - x0),(x0 - r2)))),(x0 + (min ((r1 - x0),(x0 - r2)))).[ 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

A55: x in dom (f | X) and

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

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

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

A59: (f | X) . x0 < ((f | X) . x0) + r by A39, 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 A41, XXREAL_0:2;

then A60: M2 in ].(((f | X) . x0) - r),(((f | X) . x0) + r).[ by A58;

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

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

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

then M1 in ].(((f | X) . x0) - r),(((f | X) . x0) + r).[ by A61;

then A62: [.M1,M2.] c= ].(((f | X) . x0) - r),(((f | X) . x0) + r).[ by A60, XXREAL_2:def 12;

A63: ex s being Real st

( s = x & x0 - (min ((r1 - x0),(x0 - r2))) < s & s < x0 + (min ((r1 - x0),(x0 - r2))) ) by A56;

then x0 < (min ((r1 - x0),(x0 - r2))) + x by XREAL_1:19;

then A64: x0 - x < ((min ((r1 - x0),(x0 - r2))) + x) - x by XREAL_1:9;

x - x0 < min ((r1 - x0),(x0 - r2)) by A63, XREAL_1:19;

then x - x0 < r1 - x0 by A54, XXREAL_0:2;

then A65: (x - x0) + x0 < (r1 - x0) + x0 by XREAL_1:6;

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

then A66: (f | X) . r1 <= (f | X) . x by A36, A65, A57, RFUNCT_2:23;

min ((r1 - x0),(x0 - r2)) <= x0 - r2 by XXREAL_0:17;

then x0 - x < x0 - r2 by A64, XXREAL_0:2;

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

then A67: (x - x0) + x0 > (r2 - x0) + x0 by XREAL_1:6;

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

then (f | X) . x <= (f | X) . r2 by A36, A67, A57, RFUNCT_2:23;

then (f | X) . x in [.M1,M2.] by A43, A49, A66;

hence (f | X) . x in N1 by A40, A62; :: thesis: verum

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

(f | X) . x in N1

consider r being Real such that

A39: r > 0 and

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

reconsider r = r as Element of REAL by XREAL_0:def 1;

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

reconsider M1 = ((f | X) . x0) - (r / 2) as Element of REAL by XREAL_0:def 1;

consider r1 being Element of REAL such that

A42: ( r1 in dom (f | X) & r1 in X ) and

A43: M1 = (f | X) . r1 by A3, A37, PARTFUN2:59;

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

then A45: M1 < (f | X) . x0 by XREAL_1:19;

A46: now :: thesis: not x0 > r1

reconsider M2 = ((f | X) . x0) + (r / 2) as Element of REAL by XREAL_0:def 1;assume A47:
x0 > r1
; :: thesis: contradiction

( x0 in X /\ (dom (f | X)) & r1 in X /\ (dom (f | X)) ) by A38, A42, XBOOLE_0:def 4;

hence contradiction by A36, A43, A45, A47, RFUNCT_2:23; :: thesis: verum

end;( x0 in X /\ (dom (f | X)) & r1 in X /\ (dom (f | X)) ) by A38, A42, XBOOLE_0:def 4;

hence contradiction by A36, A43, A45, A47, RFUNCT_2:23; :: thesis: verum

consider r2 being Element of REAL such that

A48: ( r2 in dom (f | X) & r2 in X ) and

A49: M2 = (f | X) . r2 by A3, A37, PARTFUN2:59;

A50: M2 > (f | X) . x0 by A39, XREAL_1:29, XREAL_1:215;

A51: now :: thesis: not r2 > x0

x0 <> r2
by A39, A49, XREAL_1:29, XREAL_1:215;assume A52:
r2 > x0
; :: thesis: contradiction

( x0 in X /\ (dom (f | X)) & r2 in X /\ (dom (f | X)) ) by A38, A48, XBOOLE_0:def 4;

hence contradiction by A36, A49, A50, A52, RFUNCT_2:23; :: thesis: verum

end;( x0 in X /\ (dom (f | X)) & r2 in X /\ (dom (f | X)) ) by A38, A48, XBOOLE_0:def 4;

hence contradiction by A36, A49, A50, A52, RFUNCT_2:23; :: thesis: verum

then x0 > r2 by A51, XXREAL_0:1;

then A53: x0 - r2 > 0 by XREAL_1:50;

set R = min ((r1 - x0),(x0 - r2));

A54: min ((r1 - x0),(x0 - r2)) <= r1 - x0 by XXREAL_0:17;

r1 <> x0 by A43, A44, XREAL_1:19;

then r1 > x0 by A46, XXREAL_0:1;

then r1 - x0 > 0 by XREAL_1:50;

then min ((r1 - x0),(x0 - r2)) > 0 by A53, XXREAL_0:15;

then reconsider N = ].(x0 - (min ((r1 - x0),(x0 - r2)))),(x0 + (min ((r1 - x0),(x0 - r2)))).[ 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

A55: x in dom (f | X) and

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

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

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

A59: (f | X) . x0 < ((f | X) . x0) + r by A39, 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 A41, XXREAL_0:2;

then A60: M2 in ].(((f | X) . x0) - r),(((f | X) . x0) + r).[ by A58;

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

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

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

then M1 in ].(((f | X) . x0) - r),(((f | X) . x0) + r).[ by A61;

then A62: [.M1,M2.] c= ].(((f | X) . x0) - r),(((f | X) . x0) + r).[ by A60, XXREAL_2:def 12;

A63: ex s being Real st

( s = x & x0 - (min ((r1 - x0),(x0 - r2))) < s & s < x0 + (min ((r1 - x0),(x0 - r2))) ) by A56;

then x0 < (min ((r1 - x0),(x0 - r2))) + x by XREAL_1:19;

then A64: x0 - x < ((min ((r1 - x0),(x0 - r2))) + x) - x by XREAL_1:9;

x - x0 < min ((r1 - x0),(x0 - r2)) by A63, XREAL_1:19;

then x - x0 < r1 - x0 by A54, XXREAL_0:2;

then A65: (x - x0) + x0 < (r1 - x0) + x0 by XREAL_1:6;

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

then A66: (f | X) . r1 <= (f | X) . x by A36, A65, A57, RFUNCT_2:23;

min ((r1 - x0),(x0 - r2)) <= x0 - r2 by XXREAL_0:17;

then x0 - x < x0 - r2 by A64, XXREAL_0:2;

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

then A67: (x - x0) + x0 > (r2 - x0) + x0 by XREAL_1:6;

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

then (f | X) . x <= (f | X) . r2 by A36, A67, A57, RFUNCT_2:23;

then (f | X) . x in [.M1,M2.] by A43, A49, A66;

hence (f | X) . x in N1 by A40, A62; :: thesis: verum