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 ;
now :: thesis: f | X is continuous
per cases ( p = g or p < g ) by ;
suppose p = g ; :: thesis: f | X is continuous
then f .: X = {p} by ;
then rng (f | X) = {p} by RELAT_1:115;
then f | X is V8() ;
hence f | X is continuous ; :: thesis: verum
end;
suppose A4: p < g ; :: thesis: f | X is continuous
now :: thesis: f | X is continuous
per cases ( f | X is non-decreasing or f | X is non-increasing ) by ;
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
proof
A6: [.p,g.] = ].p,g.[ \/ {p,g} by ;
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:
A9: (f | X) . x0 in (f | X) .: X by ;
reconsider x0 = x0 as Real ;
(f | X) . x0 in [.p,g.] by ;
then A10: ( (f | X) . x0 in ].p,g.[ or (f | X) . x0 in {p,g} ) by ;
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
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

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 ].p,g.[ or (f | X) . x0 = p or (f | X) . x0 = g ) by ;
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

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 ;
set M2 = ((f | X) . x0) + (r / 2);
A18: (f | X) . x0 < ((f | X) . x0) + (r / 2) by ;
A19: (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 ((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 ;
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 ;
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 ;
((f | X) . x0) - (r / 2) < (f | X) . x0 by ;
then ((f | X) . x0) - (r / 2) < ((f | X) . x0) + r by ;
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 ;
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 ;
A28: (f | X) . x0 < ((f | X) . x0) + (r / 2) by ;
then A29: ((f | X) . x0) - (r / 2) < (f | X) . x0 by XREAL_1:19;
A30: now :: thesis: not x0 < x1
assume A31: x0 < x1 ; :: thesis: contradiction
( x0 in X /\ (dom (f | X)) & x1 in X /\ (dom (f | X)) ) by ;
hence contradiction by A5, A27, A29, A31, RFUNCT_2:22; :: thesis: verum
end;
A32: ((f | X) . x0) + (r / 2) > (f | X) . x0 by ;
A33: now :: thesis: not x2 < x0
assume A34: x2 < x0 ; :: thesis: contradiction
( x0 in X /\ (dom (f | X)) & x2 in X /\ (dom (f | X)) ) by ;
hence contradiction by A5, A22, A32, A34, RFUNCT_2:22; :: thesis: verum
end;
x0 <> x2 by ;
then x0 < x2 by ;
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 ;
then x1 < x0 by ;
then x0 - x1 > 0 by XREAL_1:50;
then min ((x0 - x1),(x2 - x0)) > 0 by ;
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 ;
x in { s where s is Real : ( x0 - (min ((x0 - x1),(x2 - x0))) < s & s < x0 + (min ((x0 - x1),(x2 - x0))) ) } by ;
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 ;
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 ;
then A43: (f | X) . x1 <= (f | X) . x by ;
x - x0 < min ((x0 - x1),(x2 - x0)) by ;
then x - x0 < x2 - x0 by ;
then A44: (x - x0) + x0 < (x2 - x0) + x0 by XREAL_1:6;
x2 in X /\ (dom (f | X)) by ;
then (f | X) . x <= (f | X) . x2 by ;
then (f | X) . x in { s where s is Real : ( ((f | X) . x0) - (r / 2) <= s & s <= ((f | X) . x0) + (r / 2) ) } by ;
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 ;
then (f | X) . x in N3 by ;
hence (f | X) . x in N1 by A13; :: thesis: verum
end;
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

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 ;
then A49: min (r,(g - p)) > 0 by ;
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 ;
then A52: p + ((min (r,(g - p))) / 2) < p + r by XREAL_1:6;
A53: p - ((min (r,(g - p))) / 2) < p by ;
- r < - ((min (r,(g - p))) / 2) by ;
then A54: p + (- r) < p + (- ((min (r,(g - p))) / 2)) by XREAL_1:6;
p < p + r by ;
then p - ((min (r,(g - p))) / 2) < p + r by ;
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 ;
min (r,(g - p)) <= g - p by XXREAL_0:17;
then (min (r,(g - p))) / 2 < g - p by ;
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 ;
A60: x1 in X /\ (dom (f | X)) by ;
now :: thesis: not x1 < x0
assume A61: x1 < x0 ; :: thesis: contradiction
( x0 in X /\ (dom (f | X)) & x1 in X /\ (dom (f | X)) ) by ;
hence contradiction by A5, A46, A57, A59, A61, RFUNCT_2:22; :: thesis: verum
end;
then x0 < x1 by ;
then reconsider N = ].(x0 - (x1 - x0)),(x0 + (x1 - 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
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 ;
then A64: ex s being Real st
( s = x & x0 - (x1 - x0) < s & s < x0 + (x1 - x0) ) ;
(f | X) . x in [.p,g.] by ;
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 ;
x in X /\ (dom (f | X)) by ;
then (f | X) . x <= p + ((min (r,(g - p))) / 2) by ;
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 ;
then p - r < p + ((min (r,(g - p))) / 2) by ;
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 ;
hence (f | X) . x in N1 by A66; :: thesis: verum
end;
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

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 ;
reconsider r = r as Real ;
set R = (min (r,(g - p))) / 2;
g - p > 0 by ;
then A71: min (r,(g - p)) > 0 by ;
then A72: (min (r,(g - p))) / 2 < min (r,(g - p)) by XREAL_1:216;
A73: g - ((min (r,(g - p))) / 2) < g by ;
min (r,(g - p)) <= g - p by XXREAL_0:17;
then (min (r,(g - p))) / 2 < g - p by ;
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 ;
A76: now :: thesis: not x0 < x1
assume A77: x0 < x1 ; :: thesis: contradiction
( x0 in X /\ (dom (f | X)) & x1 in X /\ (dom (f | X)) ) by ;
hence contradiction by A5, A67, A73, A75, A77, RFUNCT_2:22; :: thesis: verum
end;
min (r,(g - p)) <= r by XXREAL_0:17;
then A78: (min (r,(g - p))) / 2 < r by ;
then A79: g + ((min (r,(g - p))) / 2) < g + r by XREAL_1:6;
- r < - ((min (r,(g - p))) / 2) by ;
then A80: g + (- r) < g + (- ((min (r,(g - p))) / 2)) by XREAL_1:6;
g < g + r by ;
then g - ((min (r,(g - p))) / 2) < g + r by ;
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 ;
A83: g < g + ((min (r,(g - p))) / 2) by ;
x1 <> x0 by ;
then x1 < x0 by ;
then reconsider N = ].(x0 - (x0 - x1)),(x0 + (x0 - x1)).[ 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
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 ;
then A86: ex s being Real st
( s = x & x0 - (x0 - x1) < s & s < x0 + (x0 - x1) ) ;
(f | X) . x in [.p,g.] by ;
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 ;
x in X /\ (dom (f | X)) by ;
then g - ((min (r,(g - p))) / 2) <= (f | X) . x by ;
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 ;
then g - r < g + ((min (r,(g - p))) / 2) by ;
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 ;
hence (f | X) . x in N1 by A88; :: thesis: verum
end;
end;
end;
then consider N being Neighbourhood of x0 such that
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;
hence f | X is_continuous_in x0 by Th4; :: thesis: verum
end;
hence f | X is continuous ; :: thesis: verum
end;
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
proof
A91: [.p,g.] = ].p,g.[ \/ {p,g} by ;
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:
A94: (f | X) . x0 in (f | X) .: X by ;
reconsider x0 = x0 as Real ;
(f | X) . x0 in [.p,g.] by ;
then A95: ( (f | X) . x0 in ].p,g.[ or (f | X) . x0 in {p,g} ) by ;
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
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

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 ].p,g.[ or (f | X) . x0 = p or (f | X) . x0 = g ) by ;
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

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 ;
set M2 = ((f | X) . x0) + (r / 2);
A103: (f | X) . x0 < ((f | X) . x0) + (r / 2) by ;
A104: (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 ((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 ;
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 ;
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 ;
((f | X) . x0) - (r / 2) < (f | X) . x0 by ;
then ((f | X) . x0) - (r / 2) < ((f | X) . x0) + r by ;
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 ;
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 ;
A113: (f | X) . x0 < ((f | X) . x0) + (r / 2) by ;
then A114: ((f | X) . x0) - (r / 2) < (f | X) . x0 by XREAL_1:19;
A115: now :: thesis: not x0 > x1
assume A116: x0 > x1 ; :: thesis: contradiction
( x0 in X /\ (dom (f | X)) & x1 in X /\ (dom (f | X)) ) by ;
hence contradiction by A90, A112, A114, A116, RFUNCT_2:23; :: thesis: verum
end;
A117: ((f | X) . x0) + (r / 2) > (f | X) . x0 by ;
A118: now :: thesis: not x2 > x0
assume A119: x2 > x0 ; :: thesis: contradiction
( x0 in X /\ (dom (f | X)) & x2 in X /\ (dom (f | X)) ) by ;
hence contradiction by A90, A107, A117, A119, RFUNCT_2:23; :: thesis: verum
end;
x0 <> x2 by ;
then x0 > x2 by ;
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 ;
then x1 > x0 by ;
then x1 - x0 > 0 by XREAL_1:50;
then min ((x1 - x0),(x0 - x2)) > 0 by ;
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 ;
x in { s where s is Real : ( x0 - (min ((x1 - x0),(x0 - x2))) < s & s < x0 + (min ((x1 - x0),(x0 - x2))) ) } by ;
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 ;
then x - x0 < x1 - x0 by ;
then A127: (x - x0) + x0 < (x1 - x0) + x0 by XREAL_1:6;
x1 in X /\ (dom (f | X)) by ;
then A128: (f | X) . x1 <= (f | X) . x by ;
min ((x1 - x0),(x0 - x2)) <= x0 - x2 by XXREAL_0:17;
then x0 - x < x0 - x2 by ;
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 ;
then (f | X) . x <= (f | X) . x2 by ;
then (f | X) . x in { s where s is Real : ( ((f | X) . x0) - (r / 2) <= s & s <= ((f | X) . x0) + (r / 2) ) } by ;
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 ;
then (f | X) . x in N3 by ;
hence (f | X) . x in N1 by A98; :: thesis: verum
end;
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

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 ;
then A134: min (r,(g - p)) > 0 by ;
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 ;
then A137: p + ((min (r,(g - p))) / 2) < p + r by XREAL_1:6;
A138: p - ((min (r,(g - p))) / 2) < p by ;
- r < - ((min (r,(g - p))) / 2) by ;
then A139: p + (- r) < p + (- ((min (r,(g - p))) / 2)) by XREAL_1:6;
p < p + r by ;
then p - ((min (r,(g - p))) / 2) < p + r by ;
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 ;
min (r,(g - p)) <= g - p by XXREAL_0:17;
then (min (r,(g - p))) / 2 < g - p by ;
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 ;
A145: x1 in X /\ (dom (f | X)) by ;
now :: thesis: not x1 > x0
assume A146: x1 > x0 ; :: thesis: contradiction
( x0 in X /\ (dom (f | X)) & x1 in X /\ (dom (f | X)) ) by ;
hence contradiction by A90, A131, A142, A144, A146, RFUNCT_2:23; :: thesis: verum
end;
then x0 > x1 by ;
then reconsider N = ].(x0 - (x0 - x1)),(x0 + (x0 - x1)).[ 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
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 ;
then A149: ex s being Real st
( s = x & x0 - (x0 - x1) < s & s < x0 + (x0 - x1) ) ;
(f | X) . x in [.p,g.] by ;
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 ;
x in X /\ (dom (f | X)) by ;
then (f | X) . x <= p + ((min (r,(g - p))) / 2) by ;
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 ;
then p - r < p + ((min (r,(g - p))) / 2) by ;
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 ;
hence (f | X) . x in N1 by A151; :: thesis: verum
end;
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

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 ;
reconsider r = r as Real ;
set R = (min (r,(g - p))) / 2;
g - p > 0 by ;
then A156: min (r,(g - p)) > 0 by ;
then A157: (min (r,(g - p))) / 2 < min (r,(g - p)) by XREAL_1:216;
A158: g - ((min (r,(g - p))) / 2) < g by ;
min (r,(g - p)) <= g - p by XXREAL_0:17;
then (min (r,(g - p))) / 2 < g - p by ;
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 ;
A161: now :: thesis: not x0 > x1
assume A162: x0 > x1 ; :: thesis: contradiction
( x0 in X /\ (dom (f | X)) & x1 in X /\ (dom (f | X)) ) by ;
hence contradiction by A90, A152, A158, A160, A162, RFUNCT_2:23; :: thesis: verum
end;
min (r,(g - p)) <= r by XXREAL_0:17;
then A163: (min (r,(g - p))) / 2 < r by ;
then A164: g + ((min (r,(g - p))) / 2) < g + r by XREAL_1:6;
- r < - ((min (r,(g - p))) / 2) by ;
then A165: g + (- r) < g + (- ((min (r,(g - p))) / 2)) by XREAL_1:6;
g < g + r by ;
then g - ((min (r,(g - p))) / 2) < g + r by ;
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 ;
A168: g < g + ((min (r,(g - p))) / 2) by ;
x1 <> x0 by ;
then x1 > x0 by ;
then reconsider N = ].(x0 - (x1 - x0)),(x0 + (x1 - 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
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 ;
then A171: ex s being Real st
( s = x & x0 - (x1 - x0) < s & s < x0 + (x1 - x0) ) ;
(f | X) . x in [.p,g.] by ;
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 ;
x in X /\ (dom (f | X)) by ;
then g - ((min (r,(g - p))) / 2) <= (f | X) . x by ;
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 ;
then g - r < g + ((min (r,(g - p))) / 2) by ;
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 ;
hence (f | X) . x in N1 by A173; :: thesis: verum
end;
end;
end;
then consider N being Neighbourhood of x0 such that
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;
hence f | X is_continuous_in x0 by Th4; :: thesis: verum
end;
hence f | X is continuous ; :: thesis: verum
end;
end;
end;
hence f | X is continuous ; :: thesis: verum
end;
end;
end;
hence f | X is continuous ; :: thesis: verum