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 A2: 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 A3: ( p <= g & 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 A3, XXREAL_0:1;

suppose p = g ; :: thesis: f | X is continuous

then f .: X = {p} by A3, XXREAL_1:17;
then A5: rng (f | X) = {p} by RELAT_1:148;
consider x1 being Real;
f | X is constant by A5;
hence f | X is continuous ; :: thesis: verum

end;

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

now

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

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

then A8: (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

let x0 be real number ; :: thesis: ( x0 in dom (f | X) implies f | X is_continuous_in x0 )
assume A10: x0 in dom (f | X) ; :: thesis: f | X is_continuous_in x0
then A9: x0 in X by RELAT_1:86;
then A11: (f | X) . x0 in (f | X) .: X by A10, FUNCT_1:def 12;
reconsider x0 = x0 as Real by XREAL_0:def 1;
A12: (f | X) .: X = f .: X by RELAT_1:162;
A13: (f | X) . x0 in [.p,g.] by A3, A11, RELAT_1:162;
[.p,g.] = ].p,g.[ \/ {p,g} by A3, XXREAL_1:128;
then A14: ( (f | X) . x0 in ].p,g.[ or (f | X) . x0 in {p,g} ) by A13, 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 A14, 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
A15: N2 c= ].p,g.[ by RCOMP_1:39;
consider N3 being Neighbourhood of (f | X) . x0 such that
A16: ( N3 c= N1 & N3 c= N2 ) by RCOMP_1:38;
consider r being real number such that
A17: ( r > 0 & N3 = ].(((f | X) . x0) - r),(((f | X) . x0) + r).[ ) by RCOMP_1:def 7;
reconsider r = r as Real by XREAL_0:def 1;
set M1 = ((f | X) . x0) - (r / 2);
set M2 = ((f | X) . x0) + (r / 2);
X: r / 2 > 0 by A17, XREAL_1:217;
then A19: ((f | X) . x0) - r < (((f | X) . x0) - r) + (r / 2) by XREAL_1:31;
A20: (f | X) . x0 < ((f | X) . x0) + (r / 2) by X, XREAL_1:31;
then A21: ((f | X) . x0) - (r / 2) < (f | X) . x0 by XREAL_1:21;
A22: (f | X) . x0 < ((f | X) . x0) + r by A17, XREAL_1:31;
then ((f | X) . x0) - (r / 2) < ((f | X) . x0) + r by A21, 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 A19;
then A23: ((f | X) . x0) - (r / 2) in ].(((f | X) . x0) - r),(((f | X) . x0) + r).[ by RCOMP_1:def 2;
r / 2 > 0 by A17, XREAL_1:217;
then A24: ((f | X) . x0) + (r / 2) < (((f | X) . x0) + (r / 2)) + (r / 2) by XREAL_1:31;
((f | X) . x0) - r < (((f | X) . x0) + r) - r by A22, XREAL_1:11;
then ((f | X) . x0) - r < ((f | X) . x0) + (r / 2) 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 A24;
then A25: ((f | X) . x0) + (r / 2) in ].(((f | X) . x0) - r),(((f | X) . x0) + r).[ by RCOMP_1:def 2;
then A26: [.(((f | X) . x0) - (r / 2)),(((f | X) . x0) + (r / 2)).] c= ].(((f | X) . x0) - r),(((f | X) . x0) + r).[ by A23, XXREAL_2:def 12;
((f | X) . x0) - (r / 2) in N2 by A16, A17, A23;
then A27: ((f | X) . x0) - (r / 2) in ].p,g.[ by A15;
].p,g.[ c= [.p,g.] by XXREAL_1:25;
then consider x1 being Real such that
A28: ( x1 in dom (f | X) & x1 in X & ((f | X) . x0) - (r / 2) = (f | X) . x1 ) by A3, A12, A27, PARTFUN2:78;
((f | X) . x0) + (r / 2) in N2 by A16, A17, A25;
then A29: ((f | X) . x0) + (r / 2) in ].p,g.[ by A15;
].p,g.[ c= [.p,g.] by XXREAL_1:25;
then consider x2 being Real such that
A30: ( x2 in dom (f | X) & x2 in X & ((f | X) . x0) + (r / 2) = (f | X) . x2 ) by A3, A12, A29, PARTFUN2:78;
set R = min (x0 - x1),(x2 - x0);
r / 2 > 0 by A17, XREAL_1:217;
then A31: (f | X) . x0 < ((f | X) . x0) + (r / 2) by XREAL_1:31;
then A32: ((f | X) . x0) - (r / 2) < (f | X) . x0 by XREAL_1:21;
A33: x1 <> x0 by A28, A31, XREAL_1:21;

now

assume A34: x0 < x1 ; :: thesis: contradiction
A35: x0 in X /\ (dom (f | X)) by A9, A10, XBOOLE_0:def 4;
x1 in X /\ (dom (f | X)) by A28, XBOOLE_0:def 4;
hence contradiction by A8, A28, A32, A34, A35, RFUNCT_2:45; :: thesis: verum

end;

then x1 < x0 by A33, XXREAL_0:1;
then A36: x0 - x1 > 0 by XREAL_1:52;
X: r / 2 > 0 by A17, XREAL_1:217;
then A37: ((f | X) . x0) + (r / 2) > (f | X) . x0 by XREAL_1:31;
A38: x0 <> x2 by A30, X, XREAL_1:31;

now

assume A39: x2 < x0 ; :: thesis: contradiction
A40: x0 in X /\ (dom (f | X)) by A9, A10, XBOOLE_0:def 4;
x2 in X /\ (dom (f | X)) by A30, XBOOLE_0:def 4;
hence contradiction by A8, A30, A37, A39, A40, RFUNCT_2:45; :: thesis: verum

end;

then x0 < x2 by A38, XXREAL_0:1;
then x2 - x0 > 0 by XREAL_1:52;
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 7;
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 A41: ( x in dom (f | X) & x in N ) ; :: thesis: (f | X) . x in N1
then x in { s where s is Real : ( x0 - (min (x0 - x1),(x2 - x0)) < s & s < x0 + (min (x0 - x1),(x2 - x0)) ) } by RCOMP_1:def 2;
then A42: 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:21;
then A43: x0 - x < ((min (x0 - x1),(x2 - x0)) + x) - x by XREAL_1:11;
min (x0 - x1),(x2 - x0) <= x0 - x1 by XXREAL_0:17;
then x0 - x < x0 - x1 by A43, XXREAL_0:2;
then - (x0 - x) > - (x0 - x1) by XREAL_1:26;
then A44: (x - x0) + x0 > (x1 - x0) + x0 by XREAL_1:8;
A45: x - x0 < min (x0 - x1),(x2 - x0) by A42, XREAL_1:21;
min (x0 - x1),(x2 - x0) <= x2 - x0 by XXREAL_0:17;
then x - x0 < x2 - x0 by A45, XXREAL_0:2;
then A46: (x - x0) + x0 < (x2 - x0) + x0 by XREAL_1:8;
A47: x in X /\ (dom (f | X)) by A41, RELAT_1:87, XBOOLE_1:28;
x2 in X /\ (dom (f | X)) by A30, XBOOLE_0:def 4;
then A48: (f | X) . x <= (f | X) . x2 by A8, A46, A47, RFUNCT_2:45;
x1 in X /\ (dom (f | X)) by A28, XBOOLE_0:def 4;
then (f | X) . x1 <= (f | X) . x by A8, A44, A47, RFUNCT_2:45;
then (f | X) . x in { s where s is Real : ( ((f | X) . x0) - (r / 2) <= s & s <= ((f | X) . x0) + (r / 2) ) } by A28, A30, A48;
then (f | X) . x in [.(((f | X) . x0) - (r / 2)),(((f | X) . x0) + (r / 2)).] by RCOMP_1:def 1;
then (f | X) . x in N3 by A17, A26;
hence (f | X) . x in N1 by A16; :: thesis: verum

end;

suppose A49: (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
A50: ( r > 0 & N1 = ].(p - r),(p + r).[ ) by RCOMP_1:def 7;
reconsider r = r as Real by XREAL_0:def 1;
set R = (min r,(g - p)) / 2;
g - p > 0 by A7, XREAL_1:52;
then A51: min r,(g - p) > 0 by A50, XXREAL_0:15;
A53: (min r,(g - p)) / 2 < min r,(g - p) by A51, XREAL_1:218;
min r,(g - p) <= r by XXREAL_0:17;
then A54: (min r,(g - p)) / 2 < r by A53, XXREAL_0:2;
then A55: p + ((min r,(g - p)) / 2) < p + r by XREAL_1:8;
A56: p - r < p by A50, XREAL_1:46;
(min r,(g - p)) / 2 > 0 by A51, XREAL_1:217;
then A57: p < p + ((min r,(g - p)) / 2) by XREAL_1:31;
then p - r < p + ((min r,(g - p)) / 2) by A56, 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 A58: p + ((min r,(g - p)) / 2) in ].(p - r),(p + r).[ by RCOMP_1:def 2;
(min r,(g - p)) / 2 > 0 by A51, XREAL_1:217;
then A59: p - ((min r,(g - p)) / 2) < p by XREAL_1:46;
p < p + r by A50, XREAL_1:31;
then A60: p - ((min r,(g - p)) / 2) < p + r by A59, XXREAL_0:2;
- r < - ((min r,(g - p)) / 2) by A54, XREAL_1:26;
then p + (- r) < p + (- ((min r,(g - p)) / 2)) by XREAL_1:8;
then p - ((min r,(g - p)) / 2) in { s where s is Real : ( p - r < s & s < p + r ) } by A60;
then p - ((min r,(g - p)) / 2) in ].(p - r),(p + r).[ by RCOMP_1:def 2;
then A61: [.(p - ((min r,(g - p)) / 2)),(p + ((min r,(g - p)) / 2)).] c= N1 by A50, A58, XXREAL_2:def 12;
min r,(g - p) <= g - p by XXREAL_0:17;
then (min r,(g - p)) / 2 < g - p by A53, XXREAL_0:2;
then p + ((min r,(g - p)) / 2) < g by XREAL_1:22;
then p + ((min r,(g - p)) / 2) in { s where s is Real : ( p < s & s < g ) } by A57;
then A62: p + ((min r,(g - p)) / 2) in ].p,g.[ by RCOMP_1:def 2;
].p,g.[ c= [.p,g.] by XXREAL_1:25;
then consider x1 being Real such that
A63: ( x1 in dom (f | X) & x1 in X & p + ((min r,(g - p)) / 2) = (f | X) . x1 ) by A3, A12, A62, PARTFUN2:78;

now

assume A64: x1 < x0 ; :: thesis: contradiction
A65: x0 in X /\ (dom (f | X)) by A9, A10, XBOOLE_0:def 4;
x1 in X /\ (dom (f | X)) by A63, XBOOLE_0:def 4;
hence contradiction by A8, A49, A57, A63, A64, A65, RFUNCT_2:45; :: thesis: verum

end;

then x0 < x1 by A49, A57, A63, XXREAL_0:1;
then reconsider N = ].(x0 - (x1 - x0)),(x0 + (x1 - x0)).[ as Neighbourhood of x0 by RCOMP_1:def 7, XREAL_1:52;
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 A66: ( x in dom (f | X) & x in N ) ; :: thesis: (f | X) . x in N1
A67: dom (f | X) c= X by RELAT_1:87;
then (f | X) . x in [.p,g.] by A3, A12, A66, FUNCT_1:def 12;
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 A68: p - ((min r,(g - p)) / 2) <= (f | X) . x by A59, XXREAL_0:2;
A69: x in X /\ (dom (f | X)) by A66, A67, XBOOLE_0:def 4;
A70: x1 in X /\ (dom (f | X)) by A63, XBOOLE_0:def 4;
x in { s where s is Real : ( x0 - (x1 - x0) < s & s < x0 + (x1 - x0) ) } by A66, RCOMP_1:def 2;
then ex s being Real st
( s = x & x0 - (x1 - x0) < s & s < x0 + (x1 - x0) ) ;
then (f | X) . x <= p + ((min r,(g - p)) / 2) by A8, A63, A69, A70, RFUNCT_2:45;
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 A68;
then (f | X) . x in [.(p - ((min r,(g - p)) / 2)),(p + ((min r,(g - p)) / 2)).] by RCOMP_1:def 1;
hence (f | X) . x in N1 by A61; :: thesis: verum

end;

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

then consider r being real number such that
A72: ( r > 0 & N1 = ].(g - r),(g + r).[ ) by RCOMP_1:def 7;
reconsider r = r as Real by XREAL_0:def 1;
set R = (min r,(g - p)) / 2;
g - p > 0 by A7, XREAL_1:52;
then A73: min r,(g - p) > 0 by A72, XXREAL_0:15;
A75: (min r,(g - p)) / 2 < min r,(g - p) by A73, XREAL_1:218;
min r,(g - p) <= r by XXREAL_0:17;
then A76: (min r,(g - p)) / 2 < r by A75, XXREAL_0:2;
then A77: g + ((min r,(g - p)) / 2) < g + r by XREAL_1:8;
A78: g - r < g by A72, XREAL_1:46;
(min r,(g - p)) / 2 > 0 by A73, XREAL_1:217;
then A79: g < g + ((min r,(g - p)) / 2) by XREAL_1:31;
then g - r < g + ((min r,(g - p)) / 2) by A78, XXREAL_0:2;
then g + ((min r,(g - p)) / 2) in { s where s is Real : ( g - r < s & s < g + r ) } by A77;
then A80: g + ((min r,(g - p)) / 2) in ].(g - r),(g + r).[ by RCOMP_1:def 2;
(min r,(g - p)) / 2 > 0 by A73, XREAL_1:217;
then A81: g - ((min r,(g - p)) / 2) < g by XREAL_1:46;
g < g + r by A72, XREAL_1:31;
then A82: g - ((min r,(g - p)) / 2) < g + r by A81, XXREAL_0:2;
- r < - ((min r,(g - p)) / 2) by A76, XREAL_1:26;
then g + (- r) < g + (- ((min r,(g - p)) / 2)) by XREAL_1:8;
then g - ((min r,(g - p)) / 2) in { s where s is Real : ( g - r < s & s < g + r ) } by A82;
then g - ((min r,(g - p)) / 2) in ].(g - r),(g + r).[ by RCOMP_1:def 2;
then A83: [.(g - ((min r,(g - p)) / 2)),(g + ((min r,(g - p)) / 2)).] c= N1 by A72, A80, XXREAL_2:def 12;
min r,(g - p) <= g - p by XXREAL_0:17;
then (min r,(g - p)) / 2 < g - p by A75, XXREAL_0:2;
then ((min r,(g - p)) / 2) + p < g by XREAL_1:22;
then g - ((min r,(g - p)) / 2) > p by XREAL_1:22;
then g - ((min r,(g - p)) / 2) in { s where s is Real : ( p < s & s < g ) } by A81;
then A84: g - ((min r,(g - p)) / 2) in ].p,g.[ by RCOMP_1:def 2;
].p,g.[ c= [.p,g.] by XXREAL_1:25;
then consider x1 being Real such that
A85: ( x1 in dom (f | X) & x1 in X & g - ((min r,(g - p)) / 2) = (f | X) . x1 ) by A3, A12, A84, PARTFUN2:78;
(min r,(g - p)) / 2 > 0 by A73, XREAL_1:217;
then A86: x1 <> x0 by A71, A85, XREAL_1:46;

now

assume A87: x0 < x1 ; :: thesis: contradiction
A88: x0 in X /\ (dom (f | X)) by A9, A10, XBOOLE_0:def 4;
x1 in X /\ (dom (f | X)) by A85, XBOOLE_0:def 4;
hence contradiction by A8, A71, A81, A85, A87, A88, RFUNCT_2:45; :: thesis: verum

end;

then x1 < x0 by A86, XXREAL_0:1;
then reconsider N = ].(x0 - (x0 - x1)),(x0 + (x0 - x1)).[ as Neighbourhood of x0 by RCOMP_1:def 7, XREAL_1:52;
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 A89: ( x in dom (f | X) & x in N ) ; :: thesis: (f | X) . x in N1
A90: dom (f | X) c= X by RELAT_1:87;
then (f | X) . x in [.p,g.] by A3, A12, A89, FUNCT_1:def 12;
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 A91: (f | X) . x <= g + ((min r,(g - p)) / 2) by A79, XXREAL_0:2;
A92: x in X /\ (dom (f | X)) by A89, A90, XBOOLE_0:def 4;
A93: x1 in X /\ (dom (f | X)) by A85, XBOOLE_0:def 4;
x in { s where s is Real : ( x0 - (x0 - x1) < s & s < x0 + (x0 - x1) ) } by A89, RCOMP_1:def 2;
then ex s being Real st
( s = x & x0 - (x0 - x1) < s & s < x0 + (x0 - x1) ) ;
then g - ((min r,(g - p)) / 2) <= (f | X) . x by A8, A85, A92, A93, RFUNCT_2:45;
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 A91;
then (f | X) . x in [.(g - ((min r,(g - p)) / 2)),(g + ((min r,(g - p)) / 2)).] by RCOMP_1:def 1;
hence (f | X) . x in N1 by A83; :: thesis: verum

end;

end;

end;

then consider N being Neighbourhood of x0 such that
A94: 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 A94; :: 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 A95: (f | X) | X is non-increasing by RELAT_1:101;
for x0 being real number st x0 in dom (f | X) holds
f | X is_continuous_in x0

proof

let x0 be real number ; :: thesis: ( x0 in dom (f | X) implies f | X is_continuous_in x0 )
assume A97: x0 in dom (f | X) ; :: thesis: f | X is_continuous_in x0
then A96: x0 in X by RELAT_1:86;
then A98: (f | X) . x0 in (f | X) .: X by A97, FUNCT_1:def 12;
reconsider x0 = x0 as Real by XREAL_0:def 1;
A99: (f | X) .: X = f .: X by RELAT_1:162;
A100: (f | X) . x0 in [.p,g.] by A3, A98, RELAT_1:162;
[.p,g.] = ].p,g.[ \/ {p,g} by A3, XXREAL_1:128;
then A101: ( (f | X) . x0 in ].p,g.[ or (f | X) . x0 in {p,g} ) by A100, 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 A101, 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
A102: N2 c= ].p,g.[ by RCOMP_1:39;
consider N3 being Neighbourhood of (f | X) . x0 such that
A103: ( N3 c= N1 & N3 c= N2 ) by RCOMP_1:38;
consider r being real number such that
A104: ( r > 0 & N3 = ].(((f | X) . x0) - r),(((f | X) . x0) + r).[ ) by RCOMP_1:def 7;
reconsider r = r as Real by XREAL_0:def 1;
set M1 = ((f | X) . x0) - (r / 2);
set M2 = ((f | X) . x0) + (r / 2);
X: r / 2 > 0 by A104, XREAL_1:217;
then A106: ((f | X) . x0) - r < (((f | X) . x0) - r) + (r / 2) by XREAL_1:31;
A107: (f | X) . x0 < ((f | X) . x0) + (r / 2) by X, XREAL_1:31;
then A108: ((f | X) . x0) - (r / 2) < (f | X) . x0 by XREAL_1:21;
A109: (f | X) . x0 < ((f | X) . x0) + r by A104, XREAL_1:31;
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 A106;
then A110: ((f | X) . x0) - (r / 2) in ].(((f | X) . x0) - r),(((f | X) . x0) + r).[ by RCOMP_1:def 2;
r / 2 > 0 by A104, XREAL_1:217;
then A111: ((f | X) . x0) + (r / 2) < (((f | X) . x0) + (r / 2)) + (r / 2) by XREAL_1:31;
((f | X) . x0) - r < (((f | X) . x0) + r) - r by A109, XREAL_1:11;
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 A111;
then A112: ((f | X) . x0) + (r / 2) in ].(((f | X) . x0) - r),(((f | X) . x0) + r).[ by RCOMP_1:def 2;
then A113: [.(((f | X) . x0) - (r / 2)),(((f | X) . x0) + (r / 2)).] c= ].(((f | X) . x0) - r),(((f | X) . x0) + r).[ by A110, XXREAL_2:def 12;
((f | X) . x0) - (r / 2) in N2 by A103, A104, A110;
then A114: ((f | X) . x0) - (r / 2) in ].p,g.[ by A102;
].p,g.[ c= [.p,g.] by XXREAL_1:25;
then consider x1 being Real such that
A115: ( x1 in dom (f | X) & x1 in X & ((f | X) . x0) - (r / 2) = (f | X) . x1 ) by A3, A99, A114, PARTFUN2:78;
((f | X) . x0) + (r / 2) in N2 by A103, A104, A112;
then A116: ((f | X) . x0) + (r / 2) in ].p,g.[ by A102;
].p,g.[ c= [.p,g.] by XXREAL_1:25;
then consider x2 being Real such that
A117: ( x2 in dom (f | X) & x2 in X & ((f | X) . x0) + (r / 2) = (f | X) . x2 ) by A3, A99, A116, PARTFUN2:78;
set R = min (x1 - x0),(x0 - x2);
r / 2 > 0 by A104, XREAL_1:217;
then A118: (f | X) . x0 < ((f | X) . x0) + (r / 2) by XREAL_1:31;
then A119: ((f | X) . x0) - (r / 2) < (f | X) . x0 by XREAL_1:21;
A120: x1 <> x0 by A115, A118, XREAL_1:21;

now

assume A121: x0 > x1 ; :: thesis: contradiction
A122: x0 in X /\ (dom (f | X)) by A96, A97, XBOOLE_0:def 4;
x1 in X /\ (dom (f | X)) by A115, XBOOLE_0:def 4;
hence contradiction by A95, A115, A119, A121, A122, RFUNCT_2:46; :: thesis: verum

end;

then x1 > x0 by A120, XXREAL_0:1;
then A123: x1 - x0 > 0 by XREAL_1:52;
X: r / 2 > 0 by A104, XREAL_1:217;
then A124: ((f | X) . x0) + (r / 2) > (f | X) . x0 by XREAL_1:31;
A125: x0 <> x2 by A117, X, XREAL_1:31;

now

assume A126: x2 > x0 ; :: thesis: contradiction
A127: x0 in X /\ (dom (f | X)) by A96, A97, XBOOLE_0:def 4;
x2 in X /\ (dom (f | X)) by A117, XBOOLE_0:def 4;
hence contradiction by A95, A117, A124, A126, A127, RFUNCT_2:46; :: thesis: verum

end;

then x0 > x2 by A125, XXREAL_0:1;
then x0 - x2 > 0 by XREAL_1:52;
then min (x1 - x0),(x0 - x2) > 0 by A123, 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 7;
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 A128: ( x in dom (f | X) & x in N ) ; :: thesis: (f | X) . x in N1
then x in { s where s is Real : ( x0 - (min (x1 - x0),(x0 - x2)) < s & s < x0 + (min (x1 - x0),(x0 - x2)) ) } by 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:21;
then A130: x0 - x < ((min (x1 - x0),(x0 - x2)) + x) - x by XREAL_1:11;
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:26;
then A131: (x - x0) + x0 > (x2 - x0) + x0 by XREAL_1:8;
A132: x - x0 < min (x1 - x0),(x0 - x2) by A129, XREAL_1:21;
min (x1 - x0),(x0 - x2) <= x1 - x0 by XXREAL_0:17;
then x - x0 < x1 - x0 by A132, XXREAL_0:2;
then A133: (x - x0) + x0 < (x1 - x0) + x0 by XREAL_1:8;
A134: x in X /\ (dom (f | X)) by A128, RELAT_1:87, XBOOLE_1:28;
x2 in X /\ (dom (f | X)) by A117, XBOOLE_0:def 4;
then A135: (f | X) . x <= (f | X) . x2 by A95, A131, A134, RFUNCT_2:46;
x1 in X /\ (dom (f | X)) by A115, XBOOLE_0:def 4;
then (f | X) . x1 <= (f | X) . x by A95, A133, A134, RFUNCT_2:46;
then (f | X) . x in { s where s is Real : ( ((f | X) . x0) - (r / 2) <= s & s <= ((f | X) . x0) + (r / 2) ) } by A115, A117, A135;
then (f | X) . x in [.(((f | X) . x0) - (r / 2)),(((f | X) . x0) + (r / 2)).] by RCOMP_1:def 1;
then (f | X) . x in N3 by A104, A113;
hence (f | X) . x in N1 by A103; :: thesis: verum

end;

suppose A136: (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
A137: ( r > 0 & N1 = ].(p - r),(p + r).[ ) by RCOMP_1:def 7;
reconsider r = r as Real by XREAL_0:def 1;
set R = (min r,(g - p)) / 2;
g - p > 0 by A7, XREAL_1:52;
then A138: min r,(g - p) > 0 by A137, XXREAL_0:15;
A140: (min r,(g - p)) / 2 < min r,(g - p) by A138, XREAL_1:218;
min r,(g - p) <= r by XXREAL_0:17;
then A141: (min r,(g - p)) / 2 < r by A140, XXREAL_0:2;
then A142: p + ((min r,(g - p)) / 2) < p + r by XREAL_1:8;
A143: p - r < p by A137, XREAL_1:46;
X: (min r,(g - p)) / 2 > 0 by A138, XREAL_1:217;
then A144: p < p + ((min r,(g - p)) / 2) by XREAL_1:31;
then p - r < p + ((min r,(g - p)) / 2) by A143, XXREAL_0:2;
then p + ((min r,(g - p)) / 2) in { s where s is Real : ( p - r < s & s < p + r ) } by A142;
then A145: p + ((min r,(g - p)) / 2) in ].(p - r),(p + r).[ by RCOMP_1:def 2;
A146: p - ((min r,(g - p)) / 2) < p by X, XREAL_1:46;
p < p + r by A137, XREAL_1:31;
then A147: p - ((min r,(g - p)) / 2) < p + r by A146, XXREAL_0:2;
- r < - ((min r,(g - p)) / 2) by A141, XREAL_1:26;
then p + (- r) < p + (- ((min r,(g - p)) / 2)) by XREAL_1:8;
then p - ((min r,(g - p)) / 2) in { s where s is Real : ( p - r < s & s < p + r ) } by A147;
then p - ((min r,(g - p)) / 2) in ].(p - r),(p + r).[ by RCOMP_1:def 2;
then A148: [.(p - ((min r,(g - p)) / 2)),(p + ((min r,(g - p)) / 2)).] c= N1 by A137, A145, XXREAL_2:def 12;
min r,(g - p) <= g - p by XXREAL_0:17;
then (min r,(g - p)) / 2 < g - p by A140, XXREAL_0:2;
then p + ((min r,(g - p)) / 2) < g by XREAL_1:22;
then p + ((min r,(g - p)) / 2) in { s where s is Real : ( p < s & s < g ) } by A144;
then A149: p + ((min r,(g - p)) / 2) in ].p,g.[ by RCOMP_1:def 2;
].p,g.[ c= [.p,g.] by XXREAL_1:25;
then consider x1 being Real such that
A150: ( x1 in dom (f | X) & x1 in X & p + ((min r,(g - p)) / 2) = (f | X) . x1 ) by A3, A99, A149, PARTFUN2:78;

now

assume A151: x1 > x0 ; :: thesis: contradiction
A152: x0 in X /\ (dom (f | X)) by A96, A97, XBOOLE_0:def 4;
x1 in X /\ (dom (f | X)) by A150, XBOOLE_0:def 4;
hence contradiction by A95, A136, A144, A150, A151, A152, RFUNCT_2:46; :: thesis: verum

end;

then x0 > x1 by A136, A144, A150, XXREAL_0:1;
then reconsider N = ].(x0 - (x0 - x1)),(x0 + (x0 - x1)).[ as Neighbourhood of x0 by RCOMP_1:def 7, XREAL_1:52;
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 A153: ( x in dom (f | X) & x in N ) ; :: thesis: (f | X) . x in N1
A154: dom (f | X) c= X by RELAT_1:87;
then (f | X) . x in [.p,g.] by A3, A99, A153, FUNCT_1:def 12;
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 A146, XXREAL_0:2;
A156: x in X /\ (dom (f | X)) by A153, A154, XBOOLE_0:def 4;
A157: x1 in X /\ (dom (f | X)) by A150, XBOOLE_0:def 4;
x in { s where s is Real : ( x0 - (x0 - x1) < s & s < x0 + (x0 - x1) ) } by A153, RCOMP_1:def 2;
then ex s being Real st
( s = x & x0 - (x0 - x1) < s & s < x0 + (x0 - x1) ) ;
then (f | X) . x <= p + ((min r,(g - p)) / 2) by A95, A150, A156, A157, RFUNCT_2:46;
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 (f | X) . x in [.(p - ((min r,(g - p)) / 2)),(p + ((min r,(g - p)) / 2)).] by RCOMP_1:def 1;
hence (f | X) . x in N1 by A148; :: thesis: verum

end;

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

then consider r being real number such that
A159: ( r > 0 & N1 = ].(g - r),(g + r).[ ) by RCOMP_1:def 7;
reconsider r = r as Real by XREAL_0:def 1;
set R = (min r,(g - p)) / 2;
g - p > 0 by A7, XREAL_1:52;
then A160: min r,(g - p) > 0 by A159, XXREAL_0:15;
A162: (min r,(g - p)) / 2 < min r,(g - p) by A160, XREAL_1:218;
min r,(g - p) <= r by XXREAL_0:17;
then A163: (min r,(g - p)) / 2 < r by A162, XXREAL_0:2;
then A164: g + ((min r,(g - p)) / 2) < g + r by XREAL_1:8;
A165: g - r < g by A159, XREAL_1:46;
X: (min r,(g - p)) / 2 > 0 by A160, XREAL_1:217;
then A166: g < g + ((min r,(g - p)) / 2) by XREAL_1:31;
then g - r < g + ((min r,(g - p)) / 2) by A165, 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 A167: g + ((min r,(g - p)) / 2) in ].(g - r),(g + r).[ by RCOMP_1:def 2;
A168: g - ((min r,(g - p)) / 2) < g by X, XREAL_1:46;
g < g + r by A159, XREAL_1:31;
then A169: g - ((min r,(g - p)) / 2) < g + r by A168, XXREAL_0:2;
- r < - ((min r,(g - p)) / 2) by A163, XREAL_1:26;
then g + (- r) < g + (- ((min r,(g - p)) / 2)) by XREAL_1:8;
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 A170: [.(g - ((min r,(g - p)) / 2)),(g + ((min r,(g - p)) / 2)).] c= N1 by A159, A167, XXREAL_2:def 12;
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:22;
then g - ((min r,(g - p)) / 2) > p by XREAL_1:22;
then g - ((min r,(g - p)) / 2) in { s where s is Real : ( p < s & s < g ) } by A168;
then A171: g - ((min r,(g - p)) / 2) in ].p,g.[ by RCOMP_1:def 2;
].p,g.[ c= [.p,g.] by XXREAL_1:25;
then consider x1 being Real such that
A172: ( x1 in dom (f | X) & x1 in X & g - ((min r,(g - p)) / 2) = (f | X) . x1 ) by A3, A99, A171, PARTFUN2:78;
A173: x1 <> x0 by A158, A172, X, XREAL_1:46;

now

assume A174: x0 > x1 ; :: thesis: contradiction
A175: x0 in X /\ (dom (f | X)) by A96, A97, XBOOLE_0:def 4;
x1 in X /\ (dom (f | X)) by A172, XBOOLE_0:def 4;
hence contradiction by A95, A158, A168, A172, A174, A175, RFUNCT_2:46; :: thesis: verum

end;

then x1 > x0 by A173, XXREAL_0:1;
then reconsider N = ].(x0 - (x1 - x0)),(x0 + (x1 - x0)).[ as Neighbourhood of x0 by RCOMP_1:def 7, XREAL_1:52;
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 A176: ( x in dom (f | X) & x in N ) ; :: thesis: (f | X) . x in N1
A177: dom (f | X) c= X by RELAT_1:87;
then (f | X) . x in [.p,g.] by A3, A99, A176, FUNCT_1:def 12;
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 A166, XXREAL_0:2;
A179: x in X /\ (dom (f | X)) by A176, A177, XBOOLE_0:def 4;
A180: x1 in X /\ (dom (f | X)) by A172, XBOOLE_0:def 4;
x in { s where s is Real : ( x0 - (x1 - x0) < s & s < x0 + (x1 - x0) ) } by A176, RCOMP_1:def 2;
then ex s being Real st
( s = x & x0 - (x1 - x0) < s & s < x0 + (x1 - x0) ) ;
then g - ((min r,(g - p)) / 2) <= (f | X) . x by A95, A172, A179, A180, RFUNCT_2:46;
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 (f | X) . x in [.(g - ((min r,(g - p)) / 2)),(g + ((min r,(g - p)) / 2)).] by RCOMP_1:def 1;
hence (f | X) . x in N1 by A170; :: thesis: verum

end;

end;

end;

then consider N being Neighbourhood of x0 such that
A181: 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 A181; :: 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