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

f | X is continuous

let f be PartFunc of REAL,REAL; :: thesis: ( X c= dom f & f | X is monotone & ex p being Real st f .: X = left_closed_halfline p implies f | X is continuous )

assume that

A1: X c= dom f and

A2: f | X is monotone ; :: thesis: ( for p being Real holds not f .: X = left_closed_halfline p or f | X is continuous )

given p being Real such that A3: f .: X = left_closed_halfline p ; :: thesis: f | X is continuous

set L = left_open_halfline p;

set l = left_closed_halfline p;

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

f | X is_continuous_in x0

f | X is continuous

let f be PartFunc of REAL,REAL; :: thesis: ( X c= dom f & f | X is monotone & ex p being Real st f .: X = left_closed_halfline p implies f | X is continuous )

assume that

A1: X c= dom f and

A2: f | X is monotone ; :: thesis: ( for p being Real holds not f .: X = left_closed_halfline p or f | X is continuous )

given p being Real such that A3: f .: X = left_closed_halfline p ; :: thesis: f | X is continuous

set L = left_open_halfline p;

set l = left_closed_halfline p;

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 )

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

A5: left_open_halfline p c= left_closed_halfline p by XXREAL_1:21;

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;

then (f | X) . x0 in (f | X) .: X by FUNCT_1:def 6;

then (f | X) . x0 in {p} \/ (left_open_halfline p) by A3, A4, XXREAL_1:423;

then A7: ( (f | X) . x0 in {p} or (f | X) . x0 in left_open_halfline p ) by XBOOLE_0:def 3;

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

A5: left_open_halfline p c= left_closed_halfline p by XXREAL_1:21;

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;

then (f | X) . x0 in (f | X) .: X by FUNCT_1:def 6;

then (f | X) . x0 in {p} \/ (left_open_halfline p) by A3, A4, XXREAL_1:423;

then A7: ( (f | X) . x0 in {p} or (f | X) . x0 in left_open_halfline p ) by XBOOLE_0:def 3;

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

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

(f | X) . r1 in N1

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

(f | X) . r1 in N1

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

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

(f | X) . r1 in N1

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

(f | X) . r1 in N1 ; :: thesis: verum

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

(f | X) . r1 in N1

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

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

(f | X) . r1 in N1end;

hence
ex N being Neighbourhood of x0 st for r1 being Real st r1 in dom (f | X) & r1 in N holds

(f | X) . r1 in N1

per 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: ex N being Neighbourhood of x0 st

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

(f | X) . r1 in N1

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

(f | X) . r1 in N1

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

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

(f | X) . r1 in N1 ; :: thesis: verum

end;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;

hence
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

per cases
( (f | X) . x0 in left_open_halfline p or (f | X) . x0 = p )
by A7, TARSKI:def 1;

end;

suppose
(f | X) . x0 in left_open_halfline 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 N2 being Neighbourhood of (f | X) . x0 such that

A9: N2 c= left_open_halfline p by RCOMP_1:18;

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

A10: N3 c= N1 and

A11: N3 c= N2 by RCOMP_1:17;

consider r being Real such that

A12: r > 0 and

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

reconsider r = r as Real ;

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

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

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

A16: (f | X) . x0 < ((f | X) . x0) + r by A12, 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 A15, XXREAL_0:2;

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

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

then ((f | X) . x0) + (r / 2) in left_open_halfline p by A9;

then consider r2 being Element of REAL such that

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

A19: ((f | X) . x0) + (r / 2) = (f | X) . r2 by A3, A4, A5, PARTFUN2:59;

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

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

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

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

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

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

then ((f | X) . x0) - (r / 2) in left_open_halfline p by A9;

then consider r1 being Element of REAL such that

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

A26: ((f | X) . x0) - (r / 2) = (f | X) . r1 by A3, A4, A5, PARTFUN2:59;

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

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

then x0 < r2 by A21, XXREAL_0:1;

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

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

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

r1 <> x0 by A26, A27, XREAL_1:19;

then r1 < x0 by A29, XXREAL_0:1;

then x0 - r1 > 0 by XREAL_1:50;

then min ((x0 - r1),(r2 - x0)) > 0 by A31, 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

A33: x in dom (f | X) and

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

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

A36: ex s being Real st

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

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

then A37: 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 A37, XXREAL_0:2;

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

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

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

then A39: (f | X) . r1 <= (f | X) . x by A8, A38, A35, RFUNCT_2:22;

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

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

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

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

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

then A41: (f | X) . x in [.(((f | X) . x0) - (r / 2)),(((f | X) . x0) + (r / 2)).] by A26, A19, A39;

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

then (f | X) . x in N3 by A13, A41;

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

end;A9: N2 c= left_open_halfline p by RCOMP_1:18;

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

A10: N3 c= N1 and

A11: N3 c= N2 by RCOMP_1:17;

consider r being Real such that

A12: r > 0 and

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

reconsider r = r as Real ;

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

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

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

A16: (f | X) . x0 < ((f | X) . x0) + r by A12, 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 A15, XXREAL_0:2;

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

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

then ((f | X) . x0) + (r / 2) in left_open_halfline p by A9;

then consider r2 being Element of REAL such that

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

A19: ((f | X) . x0) + (r / 2) = (f | X) . r2 by A3, A4, A5, PARTFUN2:59;

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

A21: now :: thesis: not r2 < x0

set M1 = ((f | X) . x0) - (r / 2);assume A22:
r2 < x0
; :: thesis: contradiction

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

hence contradiction by A8, A19, A20, A22, RFUNCT_2:22; :: thesis: verum

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

hence contradiction by A8, A19, A20, A22, RFUNCT_2:22; :: thesis: verum

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

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

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

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

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

then ((f | X) . x0) - (r / 2) in left_open_halfline p by A9;

then consider r1 being Element of REAL such that

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

A26: ((f | X) . x0) - (r / 2) = (f | X) . r1 by A3, A4, A5, PARTFUN2:59;

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

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

A29: now :: thesis: not x0 < r1

x0 <> r2
by A12, A19, XREAL_1:29, XREAL_1:215;assume A30:
x0 < r1
; :: thesis: contradiction

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

hence contradiction by A8, A26, A28, A30, RFUNCT_2:22; :: thesis: verum

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

hence contradiction by A8, A26, A28, A30, RFUNCT_2:22; :: thesis: verum

then x0 < r2 by A21, XXREAL_0:1;

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

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

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

r1 <> x0 by A26, A27, XREAL_1:19;

then r1 < x0 by A29, XXREAL_0:1;

then x0 - r1 > 0 by XREAL_1:50;

then min ((x0 - r1),(r2 - x0)) > 0 by A31, 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

A33: x in dom (f | X) and

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

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

A36: ex s being Real st

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

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

then A37: 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 A37, XXREAL_0:2;

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

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

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

then A39: (f | X) . r1 <= (f | X) . x by A8, A38, A35, RFUNCT_2:22;

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

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

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

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

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

then A41: (f | X) . x in [.(((f | X) . x0) - (r / 2)),(((f | X) . x0) + (r / 2)).] by A26, A19, A39;

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

then (f | X) . x in N3 by A13, A41;

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

suppose A42:
(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

A43: r > 0 and

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

reconsider r = r as Real ;

set R = r / 2;

A45: p < p + (r / 2) by A43, XREAL_1:29, XREAL_1:215;

A46: p - (r / 2) < p by A43, XREAL_1:44, XREAL_1:215;

then p - (r / 2) in { s where s is Real : s < p } ;

then p - (r / 2) in left_open_halfline p by XXREAL_1:229;

then consider r1 being Element of REAL such that

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

A48: p - (r / 2) = (f | X) . r1 by A3, A4, A5, PARTFUN2:59;

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

then r1 < x0 by A50, XXREAL_0:1;

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

A52: x in dom (f | X) and

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

A54: ex s being Real st

( s = x & x0 - (x0 - r1) < s & s < x0 + (x0 - r1) ) by A53;

A55: r / 2 < r by A43, XREAL_1:216;

then A56: p - r < p - (r / 2) by XREAL_1:15;

(f | X) . x in left_closed_halfline p by A3, A4, A52, FUNCT_1:def 6;

then (f | X) . x in { s where s is Real : s <= p } by XXREAL_1:231;

then ex s being Real st

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

then A57: (f | X) . x <= p + (r / 2) by A45, XXREAL_0:2;

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

then p - (r / 2) <= (f | X) . x by A8, A48, A49, A54, RFUNCT_2:22;

then A58: (f | X) . x in [.(p - (r / 2)),(p + (r / 2)).] by A57;

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

then p - (r / 2) < p + r by A46, XXREAL_0:2;

then A59: p - (r / 2) in ].(p - r),(p + r).[ by A56;

A60: p + (r / 2) < p + r by A55, XREAL_1:6;

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

then p - r < p + (r / 2) by A45, XXREAL_0:2;

then p + (r / 2) in ].(p - r),(p + r).[ by A60;

then [.(p - (r / 2)),(p + (r / 2)).] c= N1 by A44, A59, XXREAL_2:def 12;

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

end;A43: r > 0 and

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

reconsider r = r as Real ;

set R = r / 2;

A45: p < p + (r / 2) by A43, XREAL_1:29, XREAL_1:215;

A46: p - (r / 2) < p by A43, XREAL_1:44, XREAL_1:215;

then p - (r / 2) in { s where s is Real : s < p } ;

then p - (r / 2) in left_open_halfline p by XXREAL_1:229;

then consider r1 being Element of REAL such that

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

A48: p - (r / 2) = (f | X) . r1 by A3, A4, A5, PARTFUN2:59;

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

A50: now :: thesis: not x0 < r1

r1 <> x0
by A42, A43, A48, XREAL_1:44, XREAL_1:215;assume A51:
x0 < r1
; :: thesis: contradiction

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

hence contradiction by A8, A42, A46, A48, A51, RFUNCT_2:22; :: thesis: verum

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

hence contradiction by A8, A42, A46, A48, A51, RFUNCT_2:22; :: thesis: verum

then r1 < x0 by A50, XXREAL_0:1;

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

A52: x in dom (f | X) and

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

A54: ex s being Real st

( s = x & x0 - (x0 - r1) < s & s < x0 + (x0 - r1) ) by A53;

A55: r / 2 < r by A43, XREAL_1:216;

then A56: p - r < p - (r / 2) by XREAL_1:15;

(f | X) . x in left_closed_halfline p by A3, A4, A52, FUNCT_1:def 6;

then (f | X) . x in { s where s is Real : s <= p } by XXREAL_1:231;

then ex s being Real st

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

then A57: (f | X) . x <= p + (r / 2) by A45, XXREAL_0:2;

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

then p - (r / 2) <= (f | X) . x by A8, A48, A49, A54, RFUNCT_2:22;

then A58: (f | X) . x in [.(p - (r / 2)),(p + (r / 2)).] by A57;

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

then p - (r / 2) < p + r by A46, XXREAL_0:2;

then A59: p - (r / 2) in ].(p - r),(p + r).[ by A56;

A60: p + (r / 2) < p + r by A55, XREAL_1:6;

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

then p - r < p + (r / 2) by A45, XXREAL_0:2;

then p + (r / 2) in ].(p - r),(p + r).[ by A60;

then [.(p - (r / 2)),(p + (r / 2)).] c= N1 by A44, A59, XXREAL_2:def 12;

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

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

(f | X) . r1 in N1 ; :: thesis: verum

suppose
f | X is non-increasing
; :: thesis: ex N being Neighbourhood of x0 st

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

(f | X) . r1 in N1

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

(f | X) . r1 in N1

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

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

(f | X) . r1 in N1 ; :: thesis: verum

end;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;

hence
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

per cases
( (f | X) . x0 in left_open_halfline p or (f | X) . x0 = p )
by A7, TARSKI:def 1;

end;

suppose
(f | X) . x0 in left_open_halfline 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 N2 being Neighbourhood of (f | X) . x0 such that

A62: N2 c= left_open_halfline p by RCOMP_1:18;

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

A63: N3 c= N1 and

A64: N3 c= N2 by RCOMP_1:17;

consider r being Real such that

A65: r > 0 and

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

reconsider r = r as Real ;

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

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

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

A69: (f | X) . x0 < ((f | X) . x0) + r by A65, 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 A68, XXREAL_0:2;

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

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

then ((f | X) . x0) + (r / 2) in left_open_halfline p by A62;

then consider r2 being Element of REAL such that

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

A72: ((f | X) . x0) + (r / 2) = (f | X) . r2 by A3, A4, A5, PARTFUN2:59;

A73: ((f | X) . x0) + (r / 2) > (f | X) . x0 by A65, XREAL_1:29, XREAL_1:215;

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

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

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

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

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

then ((f | X) . x0) - (r / 2) in left_open_halfline p by A62;

then consider r1 being Element of REAL such that

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

A79: ((f | X) . x0) - (r / 2) = (f | X) . r1 by A3, A4, A5, PARTFUN2:59;

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

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

then x0 > r2 by A74, XXREAL_0:1;

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

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

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

r1 <> x0 by A79, A80, XREAL_1:19;

then r1 > x0 by A82, XXREAL_0:1;

then r1 - x0 > 0 by XREAL_1:50;

then min ((r1 - x0),(x0 - r2)) > 0 by A84, 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

A86: x in dom (f | X) and

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

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

A89: ex s being Real st

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

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

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

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

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

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

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

then A92: (f | X) . r1 <= (f | X) . x by A61, A91, A88, RFUNCT_2:23;

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

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

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

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

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

then (f | X) . x <= (f | X) . r2 by A61, A93, A88, RFUNCT_2:23;

then A94: (f | X) . x in [.(((f | X) . x0) - (r / 2)),(((f | X) . x0) + (r / 2)).] by A79, A72, A92;

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

then (f | X) . x in N3 by A66, A94;

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

end;A62: N2 c= left_open_halfline p by RCOMP_1:18;

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

A63: N3 c= N1 and

A64: N3 c= N2 by RCOMP_1:17;

consider r being Real such that

A65: r > 0 and

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

reconsider r = r as Real ;

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

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

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

A69: (f | X) . x0 < ((f | X) . x0) + r by A65, 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 A68, XXREAL_0:2;

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

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

then ((f | X) . x0) + (r / 2) in left_open_halfline p by A62;

then consider r2 being Element of REAL such that

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

A72: ((f | X) . x0) + (r / 2) = (f | X) . r2 by A3, A4, A5, PARTFUN2:59;

A73: ((f | X) . x0) + (r / 2) > (f | X) . x0 by A65, XREAL_1:29, XREAL_1:215;

A74: now :: thesis: not r2 > x0

set M1 = ((f | X) . x0) - (r / 2);assume A75:
r2 > x0
; :: thesis: contradiction

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

hence contradiction by A61, A72, A73, A75, RFUNCT_2:23; :: thesis: verum

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

hence contradiction by A61, A72, A73, A75, RFUNCT_2:23; :: thesis: verum

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

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

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

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

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

then ((f | X) . x0) - (r / 2) in left_open_halfline p by A62;

then consider r1 being Element of REAL such that

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

A79: ((f | X) . x0) - (r / 2) = (f | X) . r1 by A3, A4, A5, PARTFUN2:59;

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

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

A82: now :: thesis: not x0 > r1

x0 <> r2
by A65, A72, XREAL_1:29, XREAL_1:215;assume A83:
x0 > r1
; :: thesis: contradiction

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

hence contradiction by A61, A79, A81, A83, RFUNCT_2:23; :: thesis: verum

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

hence contradiction by A61, A79, A81, A83, RFUNCT_2:23; :: thesis: verum

then x0 > r2 by A74, XXREAL_0:1;

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

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

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

r1 <> x0 by A79, A80, XREAL_1:19;

then r1 > x0 by A82, XXREAL_0:1;

then r1 - x0 > 0 by XREAL_1:50;

then min ((r1 - x0),(x0 - r2)) > 0 by A84, 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

A86: x in dom (f | X) and

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

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

A89: ex s being Real st

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

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

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

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

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

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

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

then A92: (f | X) . r1 <= (f | X) . x by A61, A91, A88, RFUNCT_2:23;

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

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

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

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

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

then (f | X) . x <= (f | X) . r2 by A61, A93, A88, RFUNCT_2:23;

then A94: (f | X) . x in [.(((f | X) . x0) - (r / 2)),(((f | X) . x0) + (r / 2)).] by A79, A72, A92;

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

then (f | X) . x in N3 by A66, A94;

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

suppose A95:
(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

A96: r > 0 and

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

reconsider r = r as Real ;

set R = r / 2;

A98: p < p + (r / 2) by A96, XREAL_1:29, XREAL_1:215;

A99: p - (r / 2) < p by A96, XREAL_1:44, XREAL_1:215;

then p - (r / 2) in { s where s is Real : s < p } ;

then p - (r / 2) in left_open_halfline p by XXREAL_1:229;

then consider r1 being Element of REAL such that

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

A101: p - (r / 2) = (f | X) . r1 by A3, A4, A5, PARTFUN2:59;

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

then r1 > x0 by A103, XXREAL_0:1;

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

A105: x in dom (f | X) and

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

A107: ex s being Real st

( s = x & x0 - (r1 - x0) < s & s < x0 + (r1 - x0) ) by A106;

A108: r / 2 < r by A96, XREAL_1:216;

then A109: p - r < p - (r / 2) by XREAL_1:15;

(f | X) . x in left_closed_halfline p by A3, A4, A105, FUNCT_1:def 6;

then (f | X) . x in { s where s is Real : s <= p } by XXREAL_1:231;

then ex s being Real st

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

then A110: (f | X) . x <= p + (r / 2) by A98, XXREAL_0:2;

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

then p - (r / 2) <= (f | X) . x by A61, A101, A102, A107, RFUNCT_2:23;

then A111: (f | X) . x in [.(p - (r / 2)),(p + (r / 2)).] by A110;

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

then p - (r / 2) < p + r by A99, XXREAL_0:2;

then A112: p - (r / 2) in ].(p - r),(p + r).[ by A109;

A113: p + (r / 2) < p + r by A108, XREAL_1:6;

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

then p - r < p + (r / 2) by A98, XXREAL_0:2;

then p + (r / 2) in ].(p - r),(p + r).[ by A113;

then [.(p - (r / 2)),(p + (r / 2)).] c= N1 by A97, A112, XXREAL_2:def 12;

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

end;A96: r > 0 and

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

reconsider r = r as Real ;

set R = r / 2;

A98: p < p + (r / 2) by A96, XREAL_1:29, XREAL_1:215;

A99: p - (r / 2) < p by A96, XREAL_1:44, XREAL_1:215;

then p - (r / 2) in { s where s is Real : s < p } ;

then p - (r / 2) in left_open_halfline p by XXREAL_1:229;

then consider r1 being Element of REAL such that

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

A101: p - (r / 2) = (f | X) . r1 by A3, A4, A5, PARTFUN2:59;

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

A103: now :: thesis: not x0 > r1

r1 <> x0
by A95, A96, A101, XREAL_1:44, XREAL_1:215;assume A104:
x0 > r1
; :: thesis: contradiction

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

hence contradiction by A61, A95, A99, A101, A104, RFUNCT_2:23; :: thesis: verum

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

hence contradiction by A61, A95, A99, A101, A104, RFUNCT_2:23; :: thesis: verum

then r1 > x0 by A103, XXREAL_0:1;

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

A105: x in dom (f | X) and

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

A107: ex s being Real st

( s = x & x0 - (r1 - x0) < s & s < x0 + (r1 - x0) ) by A106;

A108: r / 2 < r by A96, XREAL_1:216;

then A109: p - r < p - (r / 2) by XREAL_1:15;

(f | X) . x in left_closed_halfline p by A3, A4, A105, FUNCT_1:def 6;

then (f | X) . x in { s where s is Real : s <= p } by XXREAL_1:231;

then ex s being Real st

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

then A110: (f | X) . x <= p + (r / 2) by A98, XXREAL_0:2;

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

then p - (r / 2) <= (f | X) . x by A61, A101, A102, A107, RFUNCT_2:23;

then A111: (f | X) . x in [.(p - (r / 2)),(p + (r / 2)).] by A110;

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

then p - (r / 2) < p + r by A99, XXREAL_0:2;

then A112: p - (r / 2) in ].(p - r),(p + r).[ by A109;

A113: p + (r / 2) < p + r by A108, XREAL_1:6;

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

then p - r < p + (r / 2) by A98, XXREAL_0:2;

then p + (r / 2) in ].(p - r),(p + r).[ by A113;

then [.(p - (r / 2)),(p + (r / 2)).] c= N1 by A97, A112, XXREAL_2:def 12;

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

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

(f | X) . r1 in N1 ; :: thesis: verum

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

(f | X) . r1 in N1 ; :: thesis: verum