let X be set ; :: thesis: for f being PartFunc of REAL,REAL st f | X is monotone & ex p, g being real number 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 number st
( p <= g & f .: X = [.p,g.] ) implies f | X is continuous )
assume A1: f | X is monotone ; :: thesis: ( for p, g being real number holds
( not p <= g or not f .: X = [.p,g.] ) or f | X is continuous )
given p, g being real number such that A2: p <= g and
A3: f .: X = [.p,g.] ; :: thesis: f | X is continuous
reconsider p = p, g = g as Real by XREAL_0:def 1;

now

per cases ( p = g or p < g ) by A2, XXREAL_0:1;

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 constant ;
hence f | X is continuous ; :: thesis: verum

end;

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

now

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

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

then A5: (f | X) | X is non-decreasing ;
for x0 being real number st x0 in dom (f | X) holds
f | X is_continuous_in x0

proof

A6: [.p,g.] = ].p,g.[ \/ {p,g} by A2, XXREAL_1:128;
let x0 be real number ; :: 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
then A9: x0 in X by RELAT_1:57;
then A10: (f | X) . x0 in (f | X) .: X by A8, FUNCT_1:def 6;
reconsider x0 = x0 as Real by XREAL_0:def 1;
(f | X) . x0 in [.p,g.] by A3, A10, RELAT_1:129;
then A11: ( (f | X) . x0 in ].p,g.[ or (f | X) . x0 in {p,g} ) by A6, XBOOLE_0:def 3;

now

let N1 be Neighbourhood of (f | X) . x0; :: thesis: ex N being Neighbourhood of x0 st
for x1 being real number st x1 in dom (f | X) & x1 in N holds
(f | X) . x1 in N1

now

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

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
A12: N2 c= ].p,g.[ by RCOMP_1:18;
A13: ].p,g.[ c= [.p,g.] by XXREAL_1:25;
consider N3 being Neighbourhood of (f | X) . x0 such that
A14: N3 c= N1 and
A15: N3 c= N2 by RCOMP_1:17;
consider r being real number such that
A16: r > 0 and
A17: N3 = ].(((f | X) . x0) - r),(((f | X) . x0) + r).[ by RCOMP_1:def 6;
reconsider r = r as Real by XREAL_0:def 1;
A18: ((f | X) . x0) + (r / 2) < (((f | X) . x0) + (r / 2)) + (r / 2) by A16, XREAL_1:29, XREAL_1:215;
set M2 = ((f | X) . x0) + (r / 2);
A19: (f | X) . x0 < ((f | X) . x0) + (r / 2) by A16, XREAL_1:29, XREAL_1:215;
A20: (f | X) . x0 < ((f | X) . x0) + r by A16, 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 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 A18;
then A21: ((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 A15, A17;
then ((f | X) . x0) + (r / 2) in ].p,g.[ by A12;
then consider x2 being Real such that
A22: ( x2 in dom (f | X) & x2 in X ) and
A23: ((f | X) . x0) + (r / 2) = (f | X) . x2 by A3, A7, A13, PARTFUN2:59;
A24: ].p,g.[ c= [.p,g.] by XXREAL_1:25;
set M1 = ((f | X) . x0) - (r / 2);
A25: ((f | X) . x0) - r < (((f | X) . x0) - r) + (r / 2) by A16, XREAL_1:29, XREAL_1:215;
((f | X) . x0) - (r / 2) < (f | X) . x0 by A19, XREAL_1:19;
then ((f | X) . x0) - (r / 2) < ((f | X) . x0) + r by A20, 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 A25;
then A26: ((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 A15, A17;
then ((f | X) . x0) - (r / 2) in ].p,g.[ by A12;
then consider x1 being Real such that
A27: ( x1 in dom (f | X) & x1 in X ) and
A28: ((f | X) . x0) - (r / 2) = (f | X) . x1 by A3, A7, A24, PARTFUN2:59;
A29: (f | X) . x0 < ((f | X) . x0) + (r / 2) by A16, XREAL_1:29, XREAL_1:215;
then A30: ((f | X) . x0) - (r / 2) < (f | X) . x0 by XREAL_1:19;

A31: now

assume A32: x0 < x1 ; :: thesis: contradiction
( x0 in X /\ (dom (f | X)) & x1 in X /\ (dom (f | X)) ) by A8, A9, A27, XBOOLE_0:def 4;
hence contradiction by A5, A28, A30, A32, RFUNCT_2:22; :: thesis: verum

end;

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

A34: now

assume A35: x2 < x0 ; :: thesis: contradiction
( x0 in X /\ (dom (f | X)) & x2 in X /\ (dom (f | X)) ) by A8, A9, A22, XBOOLE_0:def 4;
hence contradiction by A5, A23, A33, A35, RFUNCT_2:22; :: thesis: verum

end;

x0 <> x2 by A16, A23, XREAL_1:29, XREAL_1:215;
then x0 < x2 by A34, XXREAL_0:1;
then A36: x2 - x0 > 0 by XREAL_1:50;
set R = min ((x0 - x1),(x2 - x0));
A37: min ((x0 - x1),(x2 - x0)) <= x2 - x0 by XXREAL_0:17;
x1 <> x0 by A28, A29, XREAL_1:19;
then x1 < x0 by A31, XXREAL_0:1;
then x0 - x1 > 0 by XREAL_1:50;
then min ((x0 - x1),(x2 - x0)) > 0 by A36, 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
A38: x in dom (f | X) and
A39: x in N ; :: thesis: (f | X) . x in N1
A40: x in X /\ (dom (f | X)) by A38, RELAT_1:58, 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 A39, RCOMP_1:def 2;
then A41: 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 A42: 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 A42, XXREAL_0:2;
then - (x0 - x) > - (x0 - x1) by XREAL_1:24;
then A43: (x - x0) + x0 > (x1 - x0) + x0 by XREAL_1:6;
x1 in X /\ (dom (f | X)) by A27, XBOOLE_0:def 4;
then A44: (f | X) . x1 <= (f | X) . x by A5, A43, A40, RFUNCT_2:22;
x - x0 < min ((x0 - x1),(x2 - x0)) by A41, XREAL_1:19;
then x - x0 < x2 - x0 by A37, XXREAL_0:2;
then A45: (x - x0) + x0 < (x2 - x0) + x0 by XREAL_1:6;
x2 in X /\ (dom (f | X)) by A22, XBOOLE_0:def 4;
then (f | X) . x <= (f | X) . x2 by A5, A45, A40, 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 A28, A23, A44;
then A46: (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 A26, A21, XXREAL_2:def 12;
then (f | X) . x in N3 by A17, A46;
hence (f | X) . x in N1 by A14; :: thesis: verum

end;

suppose A47: (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 number such that
A48: r > 0 and
A49: N1 = ].(p - r),(p + r).[ by RCOMP_1:def 6;
reconsider r = r as Real by XREAL_0:def 1;
set R = (min (r,(g - p))) / 2;
g - p > 0 by A4, XREAL_1:50;
then A50: min (r,(g - p)) > 0 by A48, XXREAL_0:15;
then A51: (min (r,(g - p))) / 2 < min (r,(g - p)) by XREAL_1:216;
min (r,(g - p)) <= r by XXREAL_0:17;
then A52: (min (r,(g - p))) / 2 < r by A51, XXREAL_0:2;
then A53: p + ((min (r,(g - p))) / 2) < p + r by XREAL_1:6;
A54: p - ((min (r,(g - p))) / 2) < p by A50, XREAL_1:44, XREAL_1:215;
- r < - ((min (r,(g - p))) / 2) by A52, XREAL_1:24;
then A55: p + (- r) < p + (- ((min (r,(g - p))) / 2)) by XREAL_1:6;
p < p + r by A48, XREAL_1:29;
then p - ((min (r,(g - p))) / 2) < p + r by A54, XXREAL_0:2;
then p - ((min (r,(g - p))) / 2) in { s where s is Real : ( p - r < s & s < p + r ) } by A55;
then A56: p - ((min (r,(g - p))) / 2) in ].(p - r),(p + r).[ by RCOMP_1:def 2;
A57: ].p,g.[ c= [.p,g.] by XXREAL_1:25;
A58: p < p + ((min (r,(g - p))) / 2) by A50, 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 A51, 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 A58;
then p + ((min (r,(g - p))) / 2) in ].p,g.[ by RCOMP_1:def 2;
then consider x1 being Real such that
A59: ( x1 in dom (f | X) & x1 in X ) and
A60: p + ((min (r,(g - p))) / 2) = (f | X) . x1 by A3, A7, A57, PARTFUN2:59;
A61: x1 in X /\ (dom (f | X)) by A59, XBOOLE_0:def 4;

now

assume A62: x1 < x0 ; :: thesis: contradiction
( x0 in X /\ (dom (f | X)) & x1 in X /\ (dom (f | X)) ) by A8, A9, A59, XBOOLE_0:def 4;
hence contradiction by A5, A47, A58, A60, A62, RFUNCT_2:22; :: thesis: verum

end;

then x0 < x1 by A47, A58, A60, 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
A63: x in dom (f | X) and
A64: 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 A64, RCOMP_1:def 2;
then A65: ex s being Real st
( s = x & x0 - (x1 - x0) < s & s < x0 + (x1 - x0) ) ;
A66: dom (f | X) c= X by RELAT_1:58;
then (f | X) . x in [.p,g.] by A3, A7, A63, 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 A67: p - ((min (r,(g - p))) / 2) <= (f | X) . x by A54, XXREAL_0:2;
x in X /\ (dom (f | X)) by A63, A66, XBOOLE_0:def 4;
then (f | X) . x <= p + ((min (r,(g - p))) / 2) by A5, A60, A61, A65, 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 A67;
then A68: (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 A48, XREAL_1:44;
then p - r < p + ((min (r,(g - p))) / 2) by A58, XXREAL_0:2;
then p + ((min (r,(g - p))) / 2) in { s where s is Real : ( p - r < s & s < p + r ) } by A53;
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 A49, A56, XXREAL_2:def 12;
hence (f | X) . x in N1 by A68; :: thesis: verum

end;

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

A70: ].p,g.[ c= [.p,g.] by XXREAL_1:25;
consider r being real number such that
A71: r > 0 and
A72: N1 = ].(g - r),(g + r).[ by A69, RCOMP_1:def 6;
reconsider r = r as Real by XREAL_0:def 1;
set R = (min (r,(g - p))) / 2;
g - p > 0 by A4, XREAL_1:50;
then A73: min (r,(g - p)) > 0 by A71, XXREAL_0:15;
then A74: (min (r,(g - p))) / 2 < min (r,(g - p)) by XREAL_1:216;
A75: g - ((min (r,(g - p))) / 2) < g by A73, 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 A74, 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 A75;
then g - ((min (r,(g - p))) / 2) in ].p,g.[ by RCOMP_1:def 2;
then consider x1 being Real such that
A76: ( x1 in dom (f | X) & x1 in X ) and
A77: g - ((min (r,(g - p))) / 2) = (f | X) . x1 by A3, A7, A70, PARTFUN2:59;

A78: now

assume A79: x0 < x1 ; :: thesis: contradiction
( x0 in X /\ (dom (f | X)) & x1 in X /\ (dom (f | X)) ) by A8, A9, A76, XBOOLE_0:def 4;
hence contradiction by A5, A69, A75, A77, A79, RFUNCT_2:22; :: thesis: verum

end;

min (r,(g - p)) <= r by XXREAL_0:17;
then A80: (min (r,(g - p))) / 2 < r by A74, XXREAL_0:2;
then A81: g + ((min (r,(g - p))) / 2) < g + r by XREAL_1:6;
- r < - ((min (r,(g - p))) / 2) by A80, XREAL_1:24;
then A82: g + (- r) < g + (- ((min (r,(g - p))) / 2)) by XREAL_1:6;
g < g + r by A71, XREAL_1:29;
then g - ((min (r,(g - p))) / 2) < g + r by A75, XXREAL_0:2;
then g - ((min (r,(g - p))) / 2) in { s where s is Real : ( g - r < s & s < g + r ) } by A82;
then A83: g - ((min (r,(g - p))) / 2) in ].(g - r),(g + r).[ by RCOMP_1:def 2;
A84: x1 in X /\ (dom (f | X)) by A76, XBOOLE_0:def 4;
A85: g < g + ((min (r,(g - p))) / 2) by A73, XREAL_1:29, XREAL_1:215;
x1 <> x0 by A69, A73, A77, XREAL_1:44, XREAL_1:215;
then x1 < x0 by A78, 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
A86: x in dom (f | X) and
A87: 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 A87, RCOMP_1:def 2;
then A88: ex s being Real st
( s = x & x0 - (x0 - x1) < s & s < x0 + (x0 - x1) ) ;
A89: dom (f | X) c= X by RELAT_1:58;
then (f | X) . x in [.p,g.] by A3, A7, A86, 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 A90: (f | X) . x <= g + ((min (r,(g - p))) / 2) by A85, XXREAL_0:2;
x in X /\ (dom (f | X)) by A86, A89, XBOOLE_0:def 4;
then g - ((min (r,(g - p))) / 2) <= (f | X) . x by A5, A77, A84, A88, 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 A90;
then A91: (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 A71, XREAL_1:44;
then g - r < g + ((min (r,(g - p))) / 2) by A85, XXREAL_0:2;
then g + ((min (r,(g - p))) / 2) in { s where s is Real : ( g - r < s & s < g + r ) } by A81;
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 A72, A83, XXREAL_2:def 12;
hence (f | X) . x in N1 by A91; :: thesis: verum

end;

end;

end;

then consider N being Neighbourhood of x0 such that
A92: 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 number st x1 in dom (f | X) & x1 in N holds
(f | X) . x1 in N1
thus for x1 being real number st x1 in dom (f | X) & x1 in N holds
(f | X) . x1 in N1 by A92; :: thesis: verum

end;

hence f | X is_continuous_in x0 by Th4; :: thesis: verum

end;

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

end;

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

then A93: (f | X) | X is non-increasing by RELAT_1:72;
for x0 being real number st x0 in dom (f | X) holds
f | X is_continuous_in x0

proof

A94: [.p,g.] = ].p,g.[ \/ {p,g} by A2, XXREAL_1:128;
let x0 be real number ; :: thesis: ( x0 in dom (f | X) implies f | X is_continuous_in x0 )
A95: (f | X) .: X = f .: X by RELAT_1:129;
assume A96: x0 in dom (f | X) ; :: thesis: f | X is_continuous_in x0
then A97: x0 in X by RELAT_1:57;
then A98: (f | X) . x0 in (f | X) .: X by A96, FUNCT_1:def 6;
reconsider x0 = x0 as Real by XREAL_0:def 1;
(f | X) . x0 in [.p,g.] by A3, A98, RELAT_1:129;
then A99: ( (f | X) . x0 in ].p,g.[ or (f | X) . x0 in {p,g} ) by A94, XBOOLE_0:def 3;

now

let N1 be Neighbourhood of (f | X) . x0; :: thesis: ex N being Neighbourhood of x0 st
for x1 being real number st x1 in dom (f | X) & x1 in N holds
(f | X) . x1 in N1

now

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

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
A100: N2 c= ].p,g.[ by RCOMP_1:18;
A101: ].p,g.[ c= [.p,g.] by XXREAL_1:25;
consider N3 being Neighbourhood of (f | X) . x0 such that
A102: N3 c= N1 and
A103: N3 c= N2 by RCOMP_1:17;
consider r being real number such that
A104: r > 0 and
A105: N3 = ].(((f | X) . x0) - r),(((f | X) . x0) + r).[ by RCOMP_1:def 6;
reconsider r = r as Real by XREAL_0:def 1;
A106: ((f | X) . x0) + (r / 2) < (((f | X) . x0) + (r / 2)) + (r / 2) by A104, XREAL_1:29, XREAL_1:215;
set M2 = ((f | X) . x0) + (r / 2);
A107: (f | X) . x0 < ((f | X) . x0) + (r / 2) by A104, XREAL_1:29, XREAL_1:215;
A108: (f | X) . x0 < ((f | X) . x0) + r by A104, 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 A107, 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 A106;
then A109: ((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 A103, A105;
then ((f | X) . x0) + (r / 2) in ].p,g.[ by A100;
then consider x2 being Real such that
A110: ( x2 in dom (f | X) & x2 in X ) and
A111: ((f | X) . x0) + (r / 2) = (f | X) . x2 by A3, A95, A101, PARTFUN2:59;
A112: ].p,g.[ c= [.p,g.] by XXREAL_1:25;
set M1 = ((f | X) . x0) - (r / 2);
A113: ((f | X) . x0) - r < (((f | X) . x0) - r) + (r / 2) by A104, XREAL_1:29, XREAL_1:215;
((f | X) . x0) - (r / 2) < (f | X) . x0 by A107, XREAL_1:19;
then ((f | X) . x0) - (r / 2) < ((f | X) . x0) + r by A108, 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 A113;
then A114: ((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 A103, A105;
then ((f | X) . x0) - (r / 2) in ].p,g.[ by A100;
then consider x1 being Real such that
A115: ( x1 in dom (f | X) & x1 in X ) and
A116: ((f | X) . x0) - (r / 2) = (f | X) . x1 by A3, A95, A112, PARTFUN2:59;
A117: (f | X) . x0 < ((f | X) . x0) + (r / 2) by A104, XREAL_1:29, XREAL_1:215;
then A118: ((f | X) . x0) - (r / 2) < (f | X) . x0 by XREAL_1:19;

A119: now

assume A120: x0 > x1 ; :: thesis: contradiction
( x0 in X /\ (dom (f | X)) & x1 in X /\ (dom (f | X)) ) by A96, A97, A115, XBOOLE_0:def 4;
hence contradiction by A93, A116, A118, A120, RFUNCT_2:23; :: thesis: verum

end;

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

A122: now

assume A123: x2 > x0 ; :: thesis: contradiction
( x0 in X /\ (dom (f | X)) & x2 in X /\ (dom (f | X)) ) by A96, A97, A110, XBOOLE_0:def 4;
hence contradiction by A93, A111, A121, A123, RFUNCT_2:23; :: thesis: verum

end;

x0 <> x2 by A104, A111, XREAL_1:29, XREAL_1:215;
then x0 > x2 by A122, XXREAL_0:1;
then A124: x0 - x2 > 0 by XREAL_1:50;
set R = min ((x1 - x0),(x0 - x2));
A125: min ((x1 - x0),(x0 - x2)) <= x1 - x0 by XXREAL_0:17;
x1 <> x0 by A116, A117, XREAL_1:19;
then x1 > x0 by A119, XXREAL_0:1;
then x1 - x0 > 0 by XREAL_1:50;
then min ((x1 - x0),(x0 - x2)) > 0 by A124, 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
A126: x in dom (f | X) and
A127: x in N ; :: thesis: (f | X) . x in N1
A128: x in X /\ (dom (f | X)) by A126, RELAT_1:58, 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 A127, RCOMP_1:def 2;
then A129: 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 A130: x0 - x < ((min ((x1 - x0),(x0 - x2))) + x) - x by XREAL_1:9;
x - x0 < min ((x1 - x0),(x0 - x2)) by A129, XREAL_1:19;
then x - x0 < x1 - x0 by A125, XXREAL_0:2;
then A131: (x - x0) + x0 < (x1 - x0) + x0 by XREAL_1:6;
x1 in X /\ (dom (f | X)) by A115, XBOOLE_0:def 4;
then A132: (f | X) . x1 <= (f | X) . x by A93, A131, A128, RFUNCT_2:23;
min ((x1 - x0),(x0 - x2)) <= x0 - x2 by XXREAL_0:17;
then x0 - x < x0 - x2 by A130, XXREAL_0:2;
then - (x0 - x) > - (x0 - x2) by XREAL_1:24;
then A133: (x - x0) + x0 > (x2 - x0) + x0 by XREAL_1:6;
x2 in X /\ (dom (f | X)) by A110, XBOOLE_0:def 4;
then (f | X) . x <= (f | X) . x2 by A93, A133, A128, 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 A116, A111, A132;
then A134: (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 A114, A109, XXREAL_2:def 12;
then (f | X) . x in N3 by A105, A134;
hence (f | X) . x in N1 by A102; :: thesis: verum

end;

suppose A135: (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 number such that
A136: r > 0 and
A137: N1 = ].(p - r),(p + r).[ by RCOMP_1:def 6;
reconsider r = r as Real by XREAL_0:def 1;
set R = (min (r,(g - p))) / 2;
g - p > 0 by A4, XREAL_1:50;
then A138: min (r,(g - p)) > 0 by A136, XXREAL_0:15;
then A139: (min (r,(g - p))) / 2 < min (r,(g - p)) by XREAL_1:216;
min (r,(g - p)) <= r by XXREAL_0:17;
then A140: (min (r,(g - p))) / 2 < r by A139, XXREAL_0:2;
then A141: p + ((min (r,(g - p))) / 2) < p + r by XREAL_1:6;
A142: p - ((min (r,(g - p))) / 2) < p by A138, XREAL_1:44, XREAL_1:215;
- r < - ((min (r,(g - p))) / 2) by A140, XREAL_1:24;
then A143: p + (- r) < p + (- ((min (r,(g - p))) / 2)) by XREAL_1:6;
p < p + r by A136, XREAL_1:29;
then p - ((min (r,(g - p))) / 2) < p + r 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 A143;
then A144: p - ((min (r,(g - p))) / 2) in ].(p - r),(p + r).[ by RCOMP_1:def 2;
A145: ].p,g.[ c= [.p,g.] by XXREAL_1:25;
A146: p < p + ((min (r,(g - p))) / 2) by A138, 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 A139, 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 A146;
then p + ((min (r,(g - p))) / 2) in ].p,g.[ by RCOMP_1:def 2;
then consider x1 being Real such that
A147: ( x1 in dom (f | X) & x1 in X ) and
A148: p + ((min (r,(g - p))) / 2) = (f | X) . x1 by A3, A95, A145, PARTFUN2:59;
A149: x1 in X /\ (dom (f | X)) by A147, XBOOLE_0:def 4;

now

assume A150: x1 > x0 ; :: thesis: contradiction
( x0 in X /\ (dom (f | X)) & x1 in X /\ (dom (f | X)) ) by A96, A97, A147, XBOOLE_0:def 4;
hence contradiction by A93, A135, A146, A148, A150, RFUNCT_2:23; :: thesis: verum

end;

then x0 > x1 by A135, A146, A148, 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
A151: x in dom (f | X) and
A152: 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 A152, RCOMP_1:def 2;
then A153: ex s being Real st
( s = x & x0 - (x0 - x1) < s & s < x0 + (x0 - x1) ) ;
A154: dom (f | X) c= X by RELAT_1:58;
then (f | X) . x in [.p,g.] by A3, A95, A151, 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 A155: p - ((min (r,(g - p))) / 2) <= (f | X) . x by A142, XXREAL_0:2;
x in X /\ (dom (f | X)) by A151, A154, XBOOLE_0:def 4;
then (f | X) . x <= p + ((min (r,(g - p))) / 2) by A93, A148, A149, A153, 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 A155;
then A156: (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 A136, XREAL_1:44;
then p - r < p + ((min (r,(g - p))) / 2) by A146, XXREAL_0:2;
then p + ((min (r,(g - p))) / 2) in { s where s is Real : ( p - r < s & s < p + r ) } by A141;
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 A137, A144, XXREAL_2:def 12;
hence (f | X) . x in N1 by A156; :: thesis: verum

end;

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

A158: ].p,g.[ c= [.p,g.] by XXREAL_1:25;
consider r being real number such that
A159: r > 0 and
A160: N1 = ].(g - r),(g + r).[ by A157, RCOMP_1:def 6;
reconsider r = r as Real by XREAL_0:def 1;
set R = (min (r,(g - p))) / 2;
g - p > 0 by A4, XREAL_1:50;
then A161: min (r,(g - p)) > 0 by A159, XXREAL_0:15;
then A162: (min (r,(g - p))) / 2 < min (r,(g - p)) by XREAL_1:216;
A163: g - ((min (r,(g - p))) / 2) < g by A161, 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 A162, 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 A163;
then g - ((min (r,(g - p))) / 2) in ].p,g.[ by RCOMP_1:def 2;
then consider x1 being Real such that
A164: ( x1 in dom (f | X) & x1 in X ) and
A165: g - ((min (r,(g - p))) / 2) = (f | X) . x1 by A3, A95, A158, PARTFUN2:59;

A166: now

assume A167: x0 > x1 ; :: thesis: contradiction
( x0 in X /\ (dom (f | X)) & x1 in X /\ (dom (f | X)) ) by A96, A97, A164, XBOOLE_0:def 4;
hence contradiction by A93, A157, A163, A165, A167, RFUNCT_2:23; :: thesis: verum

end;

min (r,(g - p)) <= r by XXREAL_0:17;
then A168: (min (r,(g - p))) / 2 < r by A162, XXREAL_0:2;
then A169: g + ((min (r,(g - p))) / 2) < g + r by XREAL_1:6;
- r < - ((min (r,(g - p))) / 2) by A168, XREAL_1:24;
then A170: g + (- r) < g + (- ((min (r,(g - p))) / 2)) by XREAL_1:6;
g < g + r by A159, XREAL_1:29;
then g - ((min (r,(g - p))) / 2) < g + r by A163, XXREAL_0:2;
then g - ((min (r,(g - p))) / 2) in { s where s is Real : ( g - r < s & s < g + r ) } by A170;
then A171: g - ((min (r,(g - p))) / 2) in ].(g - r),(g + r).[ by RCOMP_1:def 2;
A172: x1 in X /\ (dom (f | X)) by A164, XBOOLE_0:def 4;
A173: g < g + ((min (r,(g - p))) / 2) by A161, XREAL_1:29, XREAL_1:215;
x1 <> x0 by A157, A161, A165, XREAL_1:44, XREAL_1:215;
then x1 > x0 by A166, 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
A174: x in dom (f | X) and
A175: 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 A175, RCOMP_1:def 2;
then A176: ex s being Real st
( s = x & x0 - (x1 - x0) < s & s < x0 + (x1 - x0) ) ;
A177: dom (f | X) c= X by RELAT_1:58;
then (f | X) . x in [.p,g.] by A3, A95, A174, 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 A178: (f | X) . x <= g + ((min (r,(g - p))) / 2) by A173, XXREAL_0:2;
x in X /\ (dom (f | X)) by A174, A177, XBOOLE_0:def 4;
then g - ((min (r,(g - p))) / 2) <= (f | X) . x by A93, A165, A172, A176, 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 A178;
then A179: (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 A159, XREAL_1:44;
then g - r < g + ((min (r,(g - p))) / 2) by A173, XXREAL_0:2;
then g + ((min (r,(g - p))) / 2) in { s where s is Real : ( g - r < s & s < g + r ) } by A169;
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 A160, A171, XXREAL_2:def 12;
hence (f | X) . x in N1 by A179; :: thesis: verum

end;

end;

end;

then consider N being Neighbourhood of x0 such that
A180: 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 number st x1 in dom (f | X) & x1 in N holds
(f | X) . x1 in N1
thus for x1 being real number st x1 in dom (f | X) & x1 in N holds
(f | X) . x1 in N1 by A180; :: thesis: verum

end;

hence f | X is_continuous_in x0 by Th4; :: thesis: verum

end;

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

end;

end;

end;

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

end;

end;

end;

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