let X be set ; :: thesis: for f being PartFunc of REAL , REAL st X c= dom f & f | X is monotone & ex p, g being Real st f .: X = ].p,g.[ holds
f | X is continuous
let f be PartFunc of REAL , REAL ; :: thesis: ( X c= dom f & f | X is monotone & ex p, g being Real st f .: X = ].p,g.[ implies f | X is continuous )
assume A1: ( X c= dom f & f | X is monotone ) ; :: thesis: ( for p, g being Real holds not f .: X = ].p,g.[ or f | X is continuous )
given p, g being Real such that A2: f .: X = ].p,g.[ ; :: thesis: f | X is continuous
set L = ].p,g.[;

now

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

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

then A3: (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 x0 in dom (f | X) ; :: thesis: f | X is_continuous_in x0
then A4: x0 in X by RELAT_1:86;
then x0 in (dom f) /\ X by A1, XBOOLE_0:def 4;
then A5: x0 in dom (f | X) by RELAT_1:90;
then A6: (f | X) . x0 in (f | X) .: X by A4, FUNCT_1:def 12;
A7: (f | X) .: X = f .: X by RELAT_1:162;
A8: (f | X) . x0 in ].p,g.[ by A2, A6, RELAT_1:162;

now

let N1 be Neighbourhood of (f | X) . x0; :: thesis: ex N being Neighbourhood of x0 st
for x being real number st x in dom (f | X) & x in N holds
(f | X) . x in N1
consider N2 being Neighbourhood of (f | X) . x0 such that
A9: N2 c= ].p,g.[ by A8, RCOMP_1:39;
consider N3 being Neighbourhood of (f | X) . x0 such that
A10: ( N3 c= N1 & N3 c= N2 ) by RCOMP_1:38;
consider r being real number such that
A11: ( 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);
A12: r / 2 > 0 by A11, XREAL_1:217;
then A13: ((f | X) . x0) - r < (((f | X) . x0) - r) + (r / 2) by XREAL_1:31;
A14: (f | X) . x0 < ((f | X) . x0) + (r / 2) by A12, XREAL_1:31;
then A15: ((f | X) . x0) - (r / 2) < (f | X) . x0 by XREAL_1:21;
A16: (f | X) . x0 < ((f | X) . x0) + r by A11, XREAL_1:31;
then ((f | X) . x0) - (r / 2) < ((f | X) . x0) + r by A15, XXREAL_0:2;
then A17: ((f | X) . x0) - (r / 2) in ].(((f | X) . x0) - r),(((f | X) . x0) + r).[ by A13;
A18: ((f | X) . x0) + (r / 2) < (((f | X) . x0) + (r / 2)) + (r / 2) by A12, XREAL_1:31;
((f | X) . x0) - r < (((f | X) . x0) + r) - r by A16, XREAL_1:11;
then ((f | X) . x0) - r < ((f | X) . x0) + (r / 2) by A14, XXREAL_0:2;
then A19: ((f | X) . x0) + (r / 2) in ].(((f | X) . x0) - r),(((f | X) . x0) + r).[ by A18;
then A20: [.(((f | X) . x0) - (r / 2)),(((f | X) . x0) + (r / 2)).] c= ].(((f | X) . x0) - r),(((f | X) . x0) + r).[ by A17, XXREAL_2:def 12;
((f | X) . x0) - (r / 2) in N2 by A10, A11, A17;
then consider r1 being Real such that
A21: ( r1 in dom (f | X) & r1 in X & ((f | X) . x0) - (r / 2) = (f | X) . r1 ) by A2, A7, A9, PARTFUN2:78;
((f | X) . x0) + (r / 2) in N2 by A10, A11, A19;
then consider r2 being Real such that
A22: ( r2 in dom (f | X) & r2 in X & ((f | X) . x0) + (r / 2) = (f | X) . r2 ) by A2, A7, A9, PARTFUN2:78;
set R = min (x0 - r1),(r2 - x0);
A23: (f | X) . x0 < ((f | X) . x0) + (r / 2) by A12, XREAL_1:31;
then A24: ((f | X) . x0) - (r / 2) < (f | X) . x0 by XREAL_1:21;
A25: r1 <> x0 by A21, A23, XREAL_1:21;

now

assume A26: x0 < r1 ; :: thesis: contradiction
A27: x0 in X /\ (dom (f | X)) by A4, A5, XBOOLE_0:def 4;
r1 in X /\ (dom (f | X)) by A21, XBOOLE_0:def 4;
hence contradiction by A3, A21, A24, A26, A27, RFUNCT_2:45; :: thesis: verum

end;

then r1 < x0 by A25, XXREAL_0:1;
then A28: x0 - r1 > 0 by XREAL_1:52;
A29: ((f | X) . x0) + (r / 2) > (f | X) . x0 by A12, XREAL_1:31;
A30: x0 <> r2 by A12, A22, XREAL_1:31;

now

assume A31: r2 < x0 ; :: thesis: contradiction
A32: x0 in X /\ (dom (f | X)) by A4, A5, XBOOLE_0:def 4;
r2 in X /\ (dom (f | X)) by A22, XBOOLE_0:def 4;
hence contradiction by A3, A22, A29, A31, A32, RFUNCT_2:45; :: thesis: verum

end;

then x0 < r2 by A30, XXREAL_0:1;
then r2 - x0 > 0 by XREAL_1:52;
then min (x0 - r1),(r2 - x0) > 0 by A28, XXREAL_0:15;
then reconsider N = ].(x0 - (min (x0 - r1),(r2 - x0))),(x0 + (min (x0 - r1),(r2 - x0))).[ as Neighbourhood of x0 by RCOMP_1:def 7;
take N = N; :: thesis: for x being real number st x in dom (f | X) & x in N holds
(f | X) . x in N1
let x be real number ; :: thesis: ( x in dom (f | X) & x in N implies (f | X) . x in N1 )
assume A33: ( x in dom (f | X) & x in N ) ; :: thesis: (f | X) . x in N1
then A34: ex s being Real st
( s = x & x0 - (min (x0 - r1),(r2 - x0)) < s & s < x0 + (min (x0 - r1),(r2 - x0)) ) ;
then x0 < (min (x0 - r1),(r2 - x0)) + x by XREAL_1:21;
then A35: x0 - x < ((min (x0 - r1),(r2 - x0)) + x) - x by XREAL_1:11;
min (x0 - r1),(r2 - x0) <= x0 - r1 by XXREAL_0:17;
then x0 - x < x0 - r1 by A35, XXREAL_0:2;
then - (x0 - x) > - (x0 - r1) by XREAL_1:26;
then A36: (x - x0) + x0 > (r1 - x0) + x0 by XREAL_1:8;
A37: x - x0 < min (x0 - r1),(r2 - x0) by A34, XREAL_1:21;
min (x0 - r1),(r2 - x0) <= r2 - x0 by XXREAL_0:17;
then x - x0 < r2 - x0 by A37, XXREAL_0:2;
then A38: (x - x0) + x0 < (r2 - x0) + x0 by XREAL_1:8;
A39: x in X /\ (dom (f | X)) by A33, RELAT_1:87, XBOOLE_1:28;
r2 in X /\ (dom (f | X)) by A22, XBOOLE_0:def 4;
then A40: (f | X) . x <= (f | X) . r2 by A3, A38, A39, RFUNCT_2:45;
r1 in X /\ (dom (f | X)) by A21, XBOOLE_0:def 4;
then (f | X) . r1 <= (f | X) . x by A3, A36, A39, RFUNCT_2:45;
then (f | X) . x in [.(((f | X) . x0) - (r / 2)),(((f | X) . x0) + (r / 2)).] by A21, A22, A40;
then (f | X) . x in N3 by A11, A20;
hence (f | X) . x in N1 by A10; :: thesis: verum

end;

hence f | X is_continuous_in x0 by FCONT_1:4; :: thesis: verum

end;

hence f | X is continuous by FCONT_1:def 2; :: thesis: verum

end;

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

then A41: (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 x0 in dom (f | X) ; :: thesis: f | X is_continuous_in x0
then A42: x0 in X by RELAT_1:86;
then x0 in (dom f) /\ X by A1, XBOOLE_0:def 4;
then A43: x0 in dom (f | X) by RELAT_1:90;
then A44: (f | X) . x0 in (f | X) .: X by A42, FUNCT_1:def 12;
A45: (f | X) .: X = f .: X by RELAT_1:162;
A46: (f | X) . x0 in ].p,g.[ by A2, A44, RELAT_1:162;

now

let N1 be Neighbourhood of (f | X) . x0; :: thesis: ex N being Neighbourhood of x0 st
for x being real number st x in dom (f | X) & x in N holds
(f | X) . x in N1
consider N2 being Neighbourhood of (f | X) . x0 such that
A47: N2 c= ].p,g.[ by A46, RCOMP_1:39;
consider N3 being Neighbourhood of (f | X) . x0 such that
A48: ( N3 c= N1 & N3 c= N2 ) by RCOMP_1:38;
consider r being real number such that
A49: ( 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);
A50: r / 2 > 0 by A49, XREAL_1:217;
then A51: ((f | X) . x0) - r < (((f | X) . x0) - r) + (r / 2) by XREAL_1:31;
A52: (f | X) . x0 < ((f | X) . x0) + (r / 2) by A50, XREAL_1:31;
then A53: ((f | X) . x0) - (r / 2) < (f | X) . x0 by XREAL_1:21;
A54: (f | X) . x0 < ((f | X) . x0) + r by A49, XREAL_1:31;
then ((f | X) . x0) - (r / 2) < ((f | X) . x0) + r by A53, XXREAL_0:2;
then A55: ((f | X) . x0) - (r / 2) in ].(((f | X) . x0) - r),(((f | X) . x0) + r).[ by A51;
A56: ((f | X) . x0) + (r / 2) < (((f | X) . x0) + (r / 2)) + (r / 2) by A50, XREAL_1:31;
((f | X) . x0) - r < (((f | X) . x0) + r) - r by A54, XREAL_1:11;
then ((f | X) . x0) - r < ((f | X) . x0) + (r / 2) by A52, XXREAL_0:2;
then A57: ((f | X) . x0) + (r / 2) in ].(((f | X) . x0) - r),(((f | X) . x0) + r).[ by A56;
then A58: [.(((f | X) . x0) - (r / 2)),(((f | X) . x0) + (r / 2)).] c= ].(((f | X) . x0) - r),(((f | X) . x0) + r).[ by A55, XXREAL_2:def 12;
((f | X) . x0) - (r / 2) in N2 by A48, A49, A55;
then consider r1 being Real such that
A59: ( r1 in dom (f | X) & r1 in X & ((f | X) . x0) - (r / 2) = (f | X) . r1 ) by A2, A45, A47, PARTFUN2:78;
((f | X) . x0) + (r / 2) in N2 by A48, A49, A57;
then consider r2 being Real such that
A60: ( r2 in dom (f | X) & r2 in X & ((f | X) . x0) + (r / 2) = (f | X) . r2 ) by A2, A45, A47, PARTFUN2:78;
set R = min (r1 - x0),(x0 - r2);
A61: (f | X) . x0 < ((f | X) . x0) + (r / 2) by A50, XREAL_1:31;
then A62: ((f | X) . x0) - (r / 2) < (f | X) . x0 by XREAL_1:21;
A63: r1 <> x0 by A59, A61, XREAL_1:21;

now

assume A64: x0 > r1 ; :: thesis: contradiction
A65: x0 in X /\ (dom (f | X)) by A42, A43, XBOOLE_0:def 4;
r1 in X /\ (dom (f | X)) by A59, XBOOLE_0:def 4;
hence contradiction by A41, A59, A62, A64, A65, RFUNCT_2:46; :: thesis: verum

end;

then r1 > x0 by A63, XXREAL_0:1;
then A66: r1 - x0 > 0 by XREAL_1:52;
A67: ((f | X) . x0) + (r / 2) > (f | X) . x0 by A50, XREAL_1:31;
A68: x0 <> r2 by A50, A60, XREAL_1:31;

now

assume A69: r2 > x0 ; :: thesis: contradiction
A70: x0 in X /\ (dom (f | X)) by A42, A43, XBOOLE_0:def 4;
r2 in X /\ (dom (f | X)) by A60, XBOOLE_0:def 4;
hence contradiction by A41, A60, A67, A69, A70, RFUNCT_2:46; :: thesis: verum

end;

then x0 > r2 by A68, XXREAL_0:1;
then x0 - r2 > 0 by XREAL_1:52;
then min (r1 - x0),(x0 - r2) > 0 by A66, XXREAL_0:15;
then reconsider N = ].(x0 - (min (r1 - x0),(x0 - r2))),(x0 + (min (r1 - x0),(x0 - r2))).[ as Neighbourhood of x0 by RCOMP_1:def 7;
take N = N; :: thesis: for x being real number st x in dom (f | X) & x in N holds
(f | X) . x in N1
let x be real number ; :: thesis: ( x in dom (f | X) & x in N implies (f | X) . x in N1 )
assume A71: ( x in dom (f | X) & x in N ) ; :: thesis: (f | X) . x in N1
then A72: ex s being Real st
( s = x & x0 - (min (r1 - x0),(x0 - r2)) < s & s < x0 + (min (r1 - x0),(x0 - r2)) ) ;
then x0 < (min (r1 - x0),(x0 - r2)) + x by XREAL_1:21;
then A73: x0 - x < ((min (r1 - x0),(x0 - r2)) + x) - x by XREAL_1:11;
min (r1 - x0),(x0 - r2) <= x0 - r2 by XXREAL_0:17;
then x0 - x < x0 - r2 by A73, XXREAL_0:2;
then - (x0 - x) > - (x0 - r2) by XREAL_1:26;
then A74: (x - x0) + x0 > (r2 - x0) + x0 by XREAL_1:8;
A75: x - x0 < min (r1 - x0),(x0 - r2) by A72, XREAL_1:21;
min (r1 - x0),(x0 - r2) <= r1 - x0 by XXREAL_0:17;
then x - x0 < r1 - x0 by A75, XXREAL_0:2;
then A76: (x - x0) + x0 < (r1 - x0) + x0 by XREAL_1:8;
A77: x in X /\ (dom (f | X)) by A71, RELAT_1:87, XBOOLE_1:28;
r2 in X /\ (dom (f | X)) by A60, XBOOLE_0:def 4;
then A78: (f | X) . x <= (f | X) . r2 by A41, A74, A77, RFUNCT_2:46;
r1 in X /\ (dom (f | X)) by A59, XBOOLE_0:def 4;
then (f | X) . r1 <= (f | X) . x by A41, A76, A77, RFUNCT_2:46;
then (f | X) . x in [.(((f | X) . x0) - (r / 2)),(((f | X) . x0) + (r / 2)).] by A59, A60, A78;
then (f | X) . x in N3 by A49, A58;
hence (f | X) . x in N1 by A48; :: thesis: verum

end;

hence f | X is_continuous_in x0 by FCONT_1:4; :: thesis: verum

end;

hence f | X is continuous by FCONT_1:def 2; :: thesis: verum

end;

end;

end;

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