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 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 :: thesis: f | X is continuous

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 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; :: 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
A9: (f | X) . x0 in (f | X) .: X by A8, FUNCT_1:def 6;
reconsider x0 = x0 as Real ;
(f | X) . x0 in [.p,g.] by A3, A9, RELAT_1:129;
then A10: ( (f | X) . x0 in ].p,g.[ or (f | X) . x0 in {p,g} ) by A6, XBOOLE_0:def 3;

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 ( (f | X) . x0 in ].p,g.[ or (f | X) . x0 = p or (f | X) . x0 = g ) by A10, 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
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 A15, XREAL_1:29, XREAL_1:215;
set M2 = ((f | X) . x0) + (r / 2);
A18: (f | X) . x0 < ((f | X) . x0) + (r / 2) by A15, XREAL_1:29, XREAL_1:215;
A19: (f | X) . x0 < ((f | X) . x0) + r by A15, 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 A18, 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 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 A14, A16;
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 A3, A7, A12, PARTFUN2:59;
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 A15, XREAL_1:29, XREAL_1:215;
((f | X) . x0) - (r / 2) < (f | X) . x0 by A18, XREAL_1:19;
then ((f | X) . x0) - (r / 2) < ((f | X) . x0) + r 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 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 A14, A16;
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 A3, A7, A23, PARTFUN2:59;
A28: (f | X) . x0 < ((f | X) . x0) + (r / 2) by A15, XREAL_1:29, XREAL_1:215;
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 A8, A26, XBOOLE_0:def 4;
hence contradiction by A5, A27, A29, A31, RFUNCT_2:22; :: thesis: verum

end;

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

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 A8, A21, XBOOLE_0:def 4;
hence contradiction by A5, A22, A32, A34, RFUNCT_2:22; :: thesis: verum

end;

x0 <> x2 by A15, A22, XREAL_1:29, XREAL_1:215;
then x0 < x2 by A33, XXREAL_0:1;
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 A27, A28, XREAL_1:19;
then x1 < x0 by A30, XXREAL_0:1;
then x0 - x1 > 0 by XREAL_1:50;
then min ((x0 - x1),(x2 - x0)) > 0 by A35, 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
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 A37, 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 A38, RCOMP_1:def 2;
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 A41, XXREAL_0:2;
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 A26, XBOOLE_0:def 4;
then A43: (f | X) . x1 <= (f | X) . x by A5, A42, A39, RFUNCT_2:22;
x - x0 < min ((x0 - x1),(x2 - x0)) by A40, XREAL_1:19;
then x - x0 < x2 - x0 by A36, XXREAL_0:2;
then A44: (x - x0) + x0 < (x2 - x0) + x0 by XREAL_1:6;
x2 in X /\ (dom (f | X)) by A21, XBOOLE_0:def 4;
then (f | X) . x <= (f | X) . x2 by A5, A44, A39, 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 A27, A22, A43;
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 A25, A20, XXREAL_2:def 12;
then (f | X) . x in N3 by A16, A45;
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 A4, XREAL_1:50;
then A49: min (r,(g - p)) > 0 by A47, XXREAL_0:15;
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 A50, XXREAL_0:2;
then A52: p + ((min (r,(g - p))) / 2) < p + r by XREAL_1:6;
A53: p - ((min (r,(g - p))) / 2) < p by A49, XREAL_1:44, XREAL_1:215;
- r < - ((min (r,(g - p))) / 2) by A51, XREAL_1:24;
then A54: p + (- r) < p + (- ((min (r,(g - p))) / 2)) by XREAL_1:6;
p < p + r by A47, XREAL_1:29;
then p - ((min (r,(g - p))) / 2) < p + r by A53, XXREAL_0:2;
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 A49, 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 A50, 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 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 A3, A7, A56, PARTFUN2:59;
A60: x1 in X /\ (dom (f | X)) by A58, XBOOLE_0:def 4;

now :: thesis: not x1 < x0

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

end;

then x0 < x1 by A46, A57, A59, 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
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 A63, RCOMP_1:def 2;
then A64: ex s being Real st
( s = x & x0 - (x1 - x0) < s & s < x0 + (x1 - x0) ) ;
(f | X) . x in [.p,g.] by A3, A7, A62, 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 A65: p - ((min (r,(g - p))) / 2) <= (f | X) . x by A53, XXREAL_0:2;
x in X /\ (dom (f | X)) by A62, XBOOLE_0:def 4;
then (f | X) . x <= p + ((min (r,(g - p))) / 2) by A5, A59, A60, A64, 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 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 A47, XREAL_1:44;
then p - r < p + ((min (r,(g - p))) / 2) by A57, XXREAL_0:2;
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 A48, A55, XXREAL_2:def 12;
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 A67, RCOMP_1:def 6;
reconsider r = r as Real ;
set R = (min (r,(g - p))) / 2;
g - p > 0 by A4, XREAL_1:50;
then A71: min (r,(g - p)) > 0 by A69, XXREAL_0:15;
then A72: (min (r,(g - p))) / 2 < min (r,(g - p)) by XREAL_1:216;
A73: g - ((min (r,(g - p))) / 2) < g by A71, 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 A72, 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 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 A3, A7, A68, PARTFUN2:59;

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 A8, A74, XBOOLE_0:def 4;
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 A72, XXREAL_0:2;
then A79: g + ((min (r,(g - p))) / 2) < g + r by XREAL_1:6;
- r < - ((min (r,(g - p))) / 2) by A78, XREAL_1:24;
then A80: g + (- r) < g + (- ((min (r,(g - p))) / 2)) by XREAL_1:6;
g < g + r by A69, XREAL_1:29;
then g - ((min (r,(g - p))) / 2) < g + r by A73, XXREAL_0:2;
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 A74, XBOOLE_0:def 4;
A83: g < g + ((min (r,(g - p))) / 2) by A71, XREAL_1:29, XREAL_1:215;
x1 <> x0 by A67, A71, A75, XREAL_1:44, XREAL_1:215;
then x1 < x0 by A76, 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
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 A85, RCOMP_1:def 2;
then A86: ex s being Real st
( s = x & x0 - (x0 - x1) < s & s < x0 + (x0 - x1) ) ;
(f | X) . x in [.p,g.] by A3, A7, A84, 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 A87: (f | X) . x <= g + ((min (r,(g - p))) / 2) by A83, XXREAL_0:2;
x in X /\ (dom (f | X)) by A84, XBOOLE_0:def 4;
then g - ((min (r,(g - p))) / 2) <= (f | X) . x by A5, A75, A82, A86, 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 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 A69, XREAL_1:44;
then g - r < g + ((min (r,(g - p))) / 2) by A83, XXREAL_0:2;
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 A70, A81, XXREAL_2:def 12;
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 A2, XXREAL_1:128;
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: f | X is_continuous_in x0
A94: (f | X) . x0 in (f | X) .: X by A93, FUNCT_1:def 6;
reconsider x0 = x0 as Real ;
(f | X) . x0 in [.p,g.] by A3, A94, RELAT_1:129;
then A95: ( (f | X) . x0 in ].p,g.[ or (f | X) . x0 in {p,g} ) by A91, XBOOLE_0:def 3;

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 ( (f | X) . x0 in ].p,g.[ or (f | X) . x0 = p or (f | X) . x0 = g ) by A95, 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
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 A100, XREAL_1:29, XREAL_1:215;
set M2 = ((f | X) . x0) + (r / 2);
A103: (f | X) . x0 < ((f | X) . x0) + (r / 2) by A100, XREAL_1:29, XREAL_1:215;
A104: (f | X) . x0 < ((f | X) . x0) + r by A100, 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 A103, 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 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 A99, A101;
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 A3, A92, A97, PARTFUN2:59;
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 A100, XREAL_1:29, XREAL_1:215;
((f | X) . x0) - (r / 2) < (f | X) . x0 by A103, XREAL_1:19;
then ((f | X) . x0) - (r / 2) < ((f | X) . x0) + r by A104, 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 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 A99, A101;
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 A3, A92, A108, PARTFUN2:59;
A113: (f | X) . x0 < ((f | X) . x0) + (r / 2) by A100, XREAL_1:29, XREAL_1:215;
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 A93, A111, XBOOLE_0:def 4;
hence contradiction by A90, A112, A114, A116, RFUNCT_2:23; :: thesis: verum

end;

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

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 A93, A106, XBOOLE_0:def 4;
hence contradiction by A90, A107, A117, A119, RFUNCT_2:23; :: thesis: verum

end;

x0 <> x2 by A100, A107, XREAL_1:29, XREAL_1:215;
then x0 > x2 by A118, XXREAL_0:1;
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 A112, A113, XREAL_1:19;
then x1 > x0 by A115, XXREAL_0:1;
then x1 - x0 > 0 by XREAL_1:50;
then min ((x1 - x0),(x0 - x2)) > 0 by A120, 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
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 A122, 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 A123, RCOMP_1:def 2;
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 A125, XREAL_1:19;
then x - x0 < x1 - x0 by A121, XXREAL_0:2;
then A127: (x - x0) + x0 < (x1 - x0) + x0 by XREAL_1:6;
x1 in X /\ (dom (f | X)) by A111, XBOOLE_0:def 4;
then A128: (f | X) . x1 <= (f | X) . x by A90, A127, A124, RFUNCT_2:23;
min ((x1 - x0),(x0 - x2)) <= x0 - x2 by XXREAL_0:17;
then x0 - x < x0 - x2 by A126, XXREAL_0:2;
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 A106, XBOOLE_0:def 4;
then (f | X) . x <= (f | X) . x2 by A90, A129, A124, 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 A112, A107, A128;
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 A110, A105, XXREAL_2:def 12;
then (f | X) . x in N3 by A101, A130;
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 A4, XREAL_1:50;
then A134: min (r,(g - p)) > 0 by A132, XXREAL_0:15;
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 A135, XXREAL_0:2;
then A137: p + ((min (r,(g - p))) / 2) < p + r by XREAL_1:6;
A138: p - ((min (r,(g - p))) / 2) < p by A134, XREAL_1:44, XREAL_1:215;
- r < - ((min (r,(g - p))) / 2) by A136, XREAL_1:24;
then A139: p + (- r) < p + (- ((min (r,(g - p))) / 2)) by XREAL_1:6;
p < p + r by A132, XREAL_1:29;
then p - ((min (r,(g - p))) / 2) < p + r by A138, XXREAL_0:2;
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 A134, 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 A135, 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 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 A3, A92, A141, PARTFUN2:59;
A145: x1 in X /\ (dom (f | X)) by A143, XBOOLE_0:def 4;

now :: thesis: not x1 > x0

assume A146: x1 > x0 ; :: thesis: contradiction
( x0 in X /\ (dom (f | X)) & x1 in X /\ (dom (f | X)) ) by A93, A143, XBOOLE_0:def 4;
hence contradiction by A90, A131, A142, A144, A146, RFUNCT_2:23; :: thesis: verum

end;

then x0 > x1 by A131, A142, A144, 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
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 A148, RCOMP_1:def 2;
then A149: ex s being Real st
( s = x & x0 - (x0 - x1) < s & s < x0 + (x0 - x1) ) ;
(f | X) . x in [.p,g.] by A3, A92, A147, 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 A150: p - ((min (r,(g - p))) / 2) <= (f | X) . x by A138, XXREAL_0:2;
x in X /\ (dom (f | X)) by A147, XBOOLE_0:def 4;
then (f | X) . x <= p + ((min (r,(g - p))) / 2) by A90, A144, A145, A149, 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 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 A132, XREAL_1:44;
then p - r < p + ((min (r,(g - p))) / 2) 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 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 A133, A140, XXREAL_2:def 12;
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 A152, RCOMP_1:def 6;
reconsider r = r as Real ;
set R = (min (r,(g - p))) / 2;
g - p > 0 by A4, XREAL_1:50;
then A156: min (r,(g - p)) > 0 by A154, XXREAL_0:15;
then A157: (min (r,(g - p))) / 2 < min (r,(g - p)) by XREAL_1:216;
A158: g - ((min (r,(g - p))) / 2) < g by A156, 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 A157, 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 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 A3, A92, A153, PARTFUN2:59;

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 A93, A159, XBOOLE_0:def 4;
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 A157, XXREAL_0:2;
then A164: g + ((min (r,(g - p))) / 2) < g + r by XREAL_1:6;
- r < - ((min (r,(g - p))) / 2) by A163, XREAL_1:24;
then A165: g + (- r) < g + (- ((min (r,(g - p))) / 2)) by XREAL_1:6;
g < g + r by A154, XREAL_1:29;
then g - ((min (r,(g - p))) / 2) < g + r by A158, XXREAL_0:2;
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 A159, XBOOLE_0:def 4;
A168: g < g + ((min (r,(g - p))) / 2) by A156, XREAL_1:29, XREAL_1:215;
x1 <> x0 by A152, A156, A160, XREAL_1:44, XREAL_1:215;
then x1 > x0 by A161, 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
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 A170, RCOMP_1:def 2;
then A171: ex s being Real st
( s = x & x0 - (x1 - x0) < s & s < x0 + (x1 - x0) ) ;
(f | X) . x in [.p,g.] by A3, A92, A169, 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 A172: (f | X) . x <= g + ((min (r,(g - p))) / 2) by A168, XXREAL_0:2;
x in X /\ (dom (f | X)) by A169, XBOOLE_0:def 4;
then g - ((min (r,(g - p))) / 2) <= (f | X) . x by A90, A160, A167, A171, 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 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 A154, XREAL_1:44;
then g - r < g + ((min (r,(g - p))) / 2) by A168, XXREAL_0:2;
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 A155, A166, XXREAL_2:def 12;
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