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
proof
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:
then x0 in X ;
then x0 in (dom f) /\ X by ;
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} \/ by ;
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
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

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 N1
per cases ( f | X is non-decreasing or f | X is non-increasing ) by ;
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

then A8: (f | X) | X is non-decreasing ;
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 N1
per cases ) . x0 in left_open_halfline p or (f | X) . x0 = p ) by ;
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

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 ;
set M2 = ((f | X) . x0) + (r / 2);
A15: (f | X) . x0 < ((f | X) . x0) + (r / 2) by ;
A16: (f | X) . x0 < ((f | X) . x0) + r by ;
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 ;
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 ;
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 ;
A20: ((f | X) . x0) + (r / 2) > (f | X) . x0 by ;
A21: now :: thesis: not r2 < x0
assume A22: r2 < x0 ; :: thesis: contradiction
( x0 in X /\ (dom (f | X)) & r2 in X /\ (dom (f | X)) ) by ;
hence contradiction by A8, A19, A20, A22, RFUNCT_2:22; :: thesis: verum
end;
set M1 = ((f | X) . x0) - (r / 2);
A23: ((f | X) . x0) - r < (((f | X) . x0) - r) + (r / 2) by ;
((f | X) . x0) - (r / 2) < (f | X) . x0 by ;
then ((f | X) . x0) - (r / 2) < ((f | X) . x0) + r by ;
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 ;
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 ;
A27: (f | X) . x0 < ((f | X) . x0) + (r / 2) by ;
then A28: ((f | X) . x0) - (r / 2) < (f | X) . x0 by XREAL_1:19;
A29: now :: thesis: not x0 < r1
assume A30: x0 < r1 ; :: thesis: contradiction
( x0 in X /\ (dom (f | X)) & r1 in X /\ (dom (f | X)) ) by ;
hence contradiction by A8, A26, A28, A30, RFUNCT_2:22; :: thesis: verum
end;
x0 <> r2 by ;
then x0 < r2 by ;
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 ;
then r1 < x0 by ;
then x0 - r1 > 0 by XREAL_1:50;
then min ((x0 - r1),(r2 - x0)) > 0 by ;
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 ;
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 ;
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 ;
then A39: (f | X) . r1 <= (f | X) . x by ;
x - x0 < min ((x0 - r1),(r2 - x0)) by ;
then x - x0 < r2 - x0 by ;
then A40: (x - x0) + x0 < (r2 - x0) + x0 by XREAL_1:6;
r2 in X /\ (dom (f | X)) by ;
then (f | X) . x <= (f | X) . r2 by ;
then A41: (f | X) . x in [.(((f | X) . x0) - (r / 2)),(((f | X) . x0) + (r / 2)).] by ;
[.(((f | X) . x0) - (r / 2)),(((f | X) . x0) + (r / 2)).] c= ].(((f | X) . x0) - r),(((f | X) . x0) + r).[ by ;
then (f | X) . x in N3 by ;
hence (f | X) . x in N1 by A10; :: thesis: verum
end;
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

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 ;
A46: p - (r / 2) < p by ;
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 ;
A49: r1 in X /\ (dom (f | X)) by ;
A50: now :: thesis: not x0 < r1
assume A51: x0 < r1 ; :: thesis: contradiction
( x0 in X /\ (dom (f | X)) & r1 in X /\ (dom (f | X)) ) by ;
hence contradiction by A8, A42, A46, A48, A51, RFUNCT_2:22; :: thesis: verum
end;
r1 <> x0 by ;
then r1 < x0 by ;
then reconsider N = ].(x0 - (x0 - r1)),(x0 + (x0 - r1)).[ as Neighbourhood of x0 by ;
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 ;
then A56: p - r < p - (r / 2) by XREAL_1:15;
(f | X) . x in left_closed_halfline p by ;
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 ;
x in X /\ (dom (f | X)) by ;
then p - (r / 2) <= (f | X) . x by ;
then A58: (f | X) . x in [.(p - (r / 2)),(p + (r / 2)).] by A57;
p < p + r by ;
then p - (r / 2) < p + r by ;
then A59: p - (r / 2) in ].(p - r),(p + r).[ by A56;
A60: p + (r / 2) < p + r by ;
p - r < p by ;
then p - r < p + (r / 2) by ;
then p + (r / 2) in ].(p - r),(p + r).[ by A60;
then [.(p - (r / 2)),(p + (r / 2)).] c= N1 by ;
hence (f | X) . x in N1 by A58; :: thesis: verum
end;
end;
end;
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 ; :: thesis: verum
end;
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

then A61: (f | X) | X is non-increasing ;
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 N1
per cases ) . x0 in left_open_halfline p or (f | X) . x0 = p ) by ;
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

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 ;
set M2 = ((f | X) . x0) + (r / 2);
A68: (f | X) . x0 < ((f | X) . x0) + (r / 2) by ;
A69: (f | X) . x0 < ((f | X) . x0) + r by ;
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 ;
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 ;
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 ;
A73: ((f | X) . x0) + (r / 2) > (f | X) . x0 by ;
A74: now :: thesis: not r2 > x0
assume A75: r2 > x0 ; :: thesis: contradiction
( x0 in X /\ (dom (f | X)) & r2 in X /\ (dom (f | X)) ) by ;
hence contradiction by A61, A72, A73, A75, RFUNCT_2:23; :: thesis: verum
end;
set M1 = ((f | X) . x0) - (r / 2);
A76: ((f | X) . x0) - r < (((f | X) . x0) - r) + (r / 2) by ;
((f | X) . x0) - (r / 2) < (f | X) . x0 by ;
then ((f | X) . x0) - (r / 2) < ((f | X) . x0) + r by ;
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 ;
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 ;
A80: (f | X) . x0 < ((f | X) . x0) + (r / 2) by ;
then A81: ((f | X) . x0) - (r / 2) < (f | X) . x0 by XREAL_1:19;
A82: now :: thesis: not x0 > r1
assume A83: x0 > r1 ; :: thesis: contradiction
( x0 in X /\ (dom (f | X)) & r1 in X /\ (dom (f | X)) ) by ;
hence contradiction by A61, A79, A81, A83, RFUNCT_2:23; :: thesis: verum
end;
x0 <> r2 by ;
then x0 > r2 by ;
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 ;
then r1 > x0 by ;
then r1 - x0 > 0 by XREAL_1:50;
then min ((r1 - x0),(x0 - r2)) > 0 by ;
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 ;
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 ;
then x - x0 < r1 - x0 by ;
then A91: (x - x0) + x0 < (r1 - x0) + x0 by XREAL_1:6;
r1 in X /\ (dom (f | X)) by ;
then A92: (f | X) . r1 <= (f | X) . x by ;
min ((r1 - x0),(x0 - r2)) <= x0 - r2 by XXREAL_0:17;
then x0 - x < x0 - r2 by ;
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 ;
then (f | X) . x <= (f | X) . r2 by ;
then A94: (f | X) . x in [.(((f | X) . x0) - (r / 2)),(((f | X) . x0) + (r / 2)).] by ;
[.(((f | X) . x0) - (r / 2)),(((f | X) . x0) + (r / 2)).] c= ].(((f | X) . x0) - r),(((f | X) . x0) + r).[ by ;
then (f | X) . x in N3 by ;
hence (f | X) . x in N1 by A63; :: thesis: verum
end;
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

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 ;
A99: p - (r / 2) < p by ;
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 ;
A102: r1 in X /\ (dom (f | X)) by ;
A103: now :: thesis: not x0 > r1
assume A104: x0 > r1 ; :: thesis: contradiction
( x0 in X /\ (dom (f | X)) & r1 in X /\ (dom (f | X)) ) by ;
hence contradiction by A61, A95, A99, A101, A104, RFUNCT_2:23; :: thesis: verum
end;
r1 <> x0 by ;
then r1 > x0 by ;
then reconsider N = ].(x0 - (r1 - x0)),(x0 + (r1 - x0)).[ as Neighbourhood of x0 by ;
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 ;
then A109: p - r < p - (r / 2) by XREAL_1:15;
(f | X) . x in left_closed_halfline p by ;
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 ;
x in X /\ (dom (f | X)) by ;
then p - (r / 2) <= (f | X) . x by ;
then A111: (f | X) . x in [.(p - (r / 2)),(p + (r / 2)).] by A110;
p < p + r by ;
then p - (r / 2) < p + r by ;
then A112: p - (r / 2) in ].(p - r),(p + r).[ by A109;
A113: p + (r / 2) < p + r by ;
p - r < p by ;
then p - r < p + (r / 2) by ;
then p + (r / 2) in ].(p - r),(p + r).[ by A113;
then [.(p - (r / 2)),(p + (r / 2)).] c= N1 by ;
hence (f | X) . x in N1 by A111; :: thesis: verum
end;
end;
end;
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 ; :: thesis: verum
end;
end;
end;
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 ; :: thesis: verum
end;
hence f | X is_continuous_in x0 by FCONT_1:4; :: thesis: verum
end;
hence f | X is continuous by FCONT_1:def 2; :: thesis: verum