let X be set ; :: thesis: for f being PartFunc of REAL ,REAL st X c= dom f & f | X is monotone & f .: X = REAL holds
f | X is continuous
let f be PartFunc of REAL ,REAL ; :: thesis: ( X c= dom f & f | X is monotone & f .: X = REAL implies f | X is continuous )
assume that
A1: X c= dom f and
A2: f | X is monotone and
A3: f .: X = REAL ; :: 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 A4: (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 )
A5: (f | X) .: X = f .: X by RELAT_1:162;
assume x0 in dom (f | X) ; :: thesis: f | X is_continuous_in x0
then A6: x0 in X by RELAT_1:86;
then x0 in (dom f) /\ X by A1, XBOOLE_0:def 4;
then A7: x0 in dom (f | X) by RELAT_1:90;

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 r being real number such that
A8: r > 0 and
A9: N1 = ].(((f | X) . x0) - r),(((f | X) . x0) + r).[ by RCOMP_1:def 7;
reconsider r = r as Real by XREAL_0:def 1;
A10: (f | X) . x0 < ((f | X) . x0) + (r / 2) by A8, XREAL_1:31, XREAL_1:217;
set M1 = ((f | X) . x0) - (r / 2);
consider r1 being Real such that
A11: ( r1 in dom (f | X) & r1 in X ) and
A12: ((f | X) . x0) - (r / 2) = (f | X) . r1 by A3, A5, PARTFUN2:78;
A13: (f | X) . x0 < ((f | X) . x0) + (r / 2) by A8, XREAL_1:31, XREAL_1:217;
then A14: ((f | X) . x0) - (r / 2) < (f | X) . x0 by XREAL_1:21;

A15: now

assume A16: x0 < r1 ; :: thesis: contradiction
( x0 in X /\ (dom (f | X)) & r1 in X /\ (dom (f | X)) ) by A6, A7, A11, XBOOLE_0:def 4;
hence contradiction by A4, A12, A14, A16, RFUNCT_2:45; :: thesis: verum

end;

set M2 = ((f | X) . x0) + (r / 2);
consider r2 being Real such that
A17: ( r2 in dom (f | X) & r2 in X ) and
A18: ((f | X) . x0) + (r / 2) = (f | X) . r2 by A3, A5, PARTFUN2:78;
A19: ((f | X) . x0) + (r / 2) > (f | X) . x0 by A8, XREAL_1:31, XREAL_1:217;

A20: now

assume A21: r2 < x0 ; :: thesis: contradiction
( x0 in X /\ (dom (f | X)) & r2 in X /\ (dom (f | X)) ) by A6, A7, A17, XBOOLE_0:def 4;
hence contradiction by A4, A18, A19, A21, RFUNCT_2:45; :: thesis: verum

end;

x0 <> r2 by A8, A18, XREAL_1:31, XREAL_1:217;
then x0 < r2 by A20, XXREAL_0:1;
then A22: r2 - x0 > 0 by XREAL_1:52;
set R = min (x0 - r1),(r2 - x0);
A23: min (x0 - r1),(r2 - x0) <= r2 - x0 by XXREAL_0:17;
r1 <> x0 by A12, A13, XREAL_1:21;
then r1 < x0 by A15, XXREAL_0:1;
then x0 - r1 > 0 by XREAL_1:52;
then min (x0 - r1),(r2 - x0) > 0 by A22, 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 that
A24: x in dom (f | X) and
A25: x in N ; :: thesis: (f | X) . x in N1
A26: x in X /\ (dom (f | X)) by A24, RELAT_1:87, XBOOLE_1:28;
A27: ((f | X) . x0) + (r / 2) < (((f | X) . x0) + (r / 2)) + (r / 2) by A8, XREAL_1:31, XREAL_1:217;
A28: (f | X) . x0 < ((f | X) . x0) + r by A8, XREAL_1:31;
then ((f | X) . x0) - r < (((f | X) . x0) + r) - r by XREAL_1:11;
then ((f | X) . x0) - r < ((f | X) . x0) + (r / 2) by A10, XXREAL_0:2;
then A29: ((f | X) . x0) + (r / 2) in ].(((f | X) . x0) - r),(((f | X) . x0) + r).[ by A27;
A30: ((f | X) . x0) - r < (((f | X) . x0) - r) + (r / 2) by A8, XREAL_1:31, XREAL_1:217;
((f | X) . x0) - (r / 2) < (f | X) . x0 by A10, XREAL_1:21;
then ((f | X) . x0) - (r / 2) < ((f | X) . x0) + r by A28, XXREAL_0:2;
then ((f | X) . x0) - (r / 2) in ].(((f | X) . x0) - r),(((f | X) . x0) + r).[ by A30;
then A31: [.(((f | X) . x0) - (r / 2)),(((f | X) . x0) + (r / 2)).] c= ].(((f | X) . x0) - r),(((f | X) . x0) + r).[ by A29, XXREAL_2:def 12;
A32: ex s being Real st
( s = x & x0 - (min (x0 - r1),(r2 - x0)) < s & s < x0 + (min (x0 - r1),(r2 - x0)) ) by A25;
then x0 < (min (x0 - r1),(r2 - x0)) + x by XREAL_1:21;
then A33: 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 A33, XXREAL_0:2;
then - (x0 - x) > - (x0 - r1) by XREAL_1:26;
then A34: (x - x0) + x0 > (r1 - x0) + x0 by XREAL_1:8;
r1 in X /\ (dom (f | X)) by A11, XBOOLE_0:def 4;
then A35: (f | X) . r1 <= (f | X) . x by A4, A34, A26, RFUNCT_2:45;
x - x0 < min (x0 - r1),(r2 - x0) by A32, XREAL_1:21;
then x - x0 < r2 - x0 by A23, XXREAL_0:2;
then A36: (x - x0) + x0 < (r2 - x0) + x0 by XREAL_1:8;
r2 in X /\ (dom (f | X)) by A17, XBOOLE_0:def 4;
then (f | X) . x <= (f | X) . r2 by A4, A36, A26, RFUNCT_2:45;
then (f | X) . x in [.(((f | X) . x0) - (r / 2)),(((f | X) . x0) + (r / 2)).] by A12, A18, A35;
hence (f | X) . x in N1 by A9, A31; :: 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 A37: (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 )
A38: (f | X) .: X = f .: X by RELAT_1:162;
assume x0 in dom (f | X) ; :: thesis: f | X is_continuous_in x0
then A39: x0 in X by RELAT_1:86;
then x0 in (dom f) /\ X by A1, XBOOLE_0:def 4;
then A40: x0 in dom (f | X) by RELAT_1:90;

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 r being real number such that
A41: r > 0 and
A42: N1 = ].(((f | X) . x0) - r),(((f | X) . x0) + r).[ by RCOMP_1:def 7;
reconsider r = r as Real by XREAL_0:def 1;
A43: (f | X) . x0 < ((f | X) . x0) + (r / 2) by A41, XREAL_1:31, XREAL_1:217;
set M1 = ((f | X) . x0) - (r / 2);
consider r1 being Real such that
A44: ( r1 in dom (f | X) & r1 in X ) and
A45: ((f | X) . x0) - (r / 2) = (f | X) . r1 by A3, A38, PARTFUN2:78;
A46: (f | X) . x0 < ((f | X) . x0) + (r / 2) by A41, XREAL_1:31, XREAL_1:217;
then A47: ((f | X) . x0) - (r / 2) < (f | X) . x0 by XREAL_1:21;

A48: now

assume A49: x0 > r1 ; :: thesis: contradiction
( x0 in X /\ (dom (f | X)) & r1 in X /\ (dom (f | X)) ) by A39, A40, A44, XBOOLE_0:def 4;
hence contradiction by A37, A45, A47, A49, RFUNCT_2:46; :: thesis: verum

end;

set M2 = ((f | X) . x0) + (r / 2);
consider r2 being Real such that
A50: ( r2 in dom (f | X) & r2 in X ) and
A51: ((f | X) . x0) + (r / 2) = (f | X) . r2 by A3, A38, PARTFUN2:78;
A52: ((f | X) . x0) + (r / 2) > (f | X) . x0 by A41, XREAL_1:31, XREAL_1:217;

A53: now

assume A54: r2 > x0 ; :: thesis: contradiction
( x0 in X /\ (dom (f | X)) & r2 in X /\ (dom (f | X)) ) by A39, A40, A50, XBOOLE_0:def 4;
hence contradiction by A37, A51, A52, A54, RFUNCT_2:46; :: thesis: verum

end;

x0 <> r2 by A41, A51, XREAL_1:31, XREAL_1:217;
then x0 > r2 by A53, XXREAL_0:1;
then A55: x0 - r2 > 0 by XREAL_1:52;
set R = min (r1 - x0),(x0 - r2);
A56: min (r1 - x0),(x0 - r2) <= r1 - x0 by XXREAL_0:17;
r1 <> x0 by A45, A46, XREAL_1:21;
then r1 > x0 by A48, XXREAL_0:1;
then r1 - x0 > 0 by XREAL_1:52;
then min (r1 - x0),(x0 - r2) > 0 by A55, 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 that
A57: x in dom (f | X) and
A58: x in N ; :: thesis: (f | X) . x in N1
A59: x in X /\ (dom (f | X)) by A57, RELAT_1:87, XBOOLE_1:28;
A60: ((f | X) . x0) + (r / 2) < (((f | X) . x0) + (r / 2)) + (r / 2) by A41, XREAL_1:31, XREAL_1:217;
A61: (f | X) . x0 < ((f | X) . x0) + r by A41, XREAL_1:31;
then ((f | X) . x0) - r < (((f | X) . x0) + r) - r by XREAL_1:11;
then ((f | X) . x0) - r < ((f | X) . x0) + (r / 2) by A43, XXREAL_0:2;
then A62: ((f | X) . x0) + (r / 2) in ].(((f | X) . x0) - r),(((f | X) . x0) + r).[ by A60;
A63: ((f | X) . x0) - r < (((f | X) . x0) - r) + (r / 2) by A41, XREAL_1:31, XREAL_1:217;
((f | X) . x0) - (r / 2) < (f | X) . x0 by A43, XREAL_1:21;
then ((f | X) . x0) - (r / 2) < ((f | X) . x0) + r by A61, XXREAL_0:2;
then ((f | X) . x0) - (r / 2) in ].(((f | X) . x0) - r),(((f | X) . x0) + r).[ by A63;
then A64: [.(((f | X) . x0) - (r / 2)),(((f | X) . x0) + (r / 2)).] c= ].(((f | X) . x0) - r),(((f | X) . x0) + r).[ by A62, XXREAL_2:def 12;
A65: ex s being Real st
( s = x & x0 - (min (r1 - x0),(x0 - r2)) < s & s < x0 + (min (r1 - x0),(x0 - r2)) ) by A58;
then x0 < (min (r1 - x0),(x0 - r2)) + x by XREAL_1:21;
then A66: x0 - x < ((min (r1 - x0),(x0 - r2)) + x) - x by XREAL_1:11;
x - x0 < min (r1 - x0),(x0 - r2) by A65, XREAL_1:21;
then x - x0 < r1 - x0 by A56, XXREAL_0:2;
then A67: (x - x0) + x0 < (r1 - x0) + x0 by XREAL_1:8;
r1 in X /\ (dom (f | X)) by A44, XBOOLE_0:def 4;
then A68: (f | X) . r1 <= (f | X) . x by A37, A67, A59, RFUNCT_2:46;
min (r1 - x0),(x0 - r2) <= x0 - r2 by XXREAL_0:17;
then x0 - x < x0 - r2 by A66, XXREAL_0:2;
then - (x0 - x) > - (x0 - r2) by XREAL_1:26;
then A69: (x - x0) + x0 > (r2 - x0) + x0 by XREAL_1:8;
r2 in X /\ (dom (f | X)) by A50, XBOOLE_0:def 4;
then (f | X) . x <= (f | X) . r2 by A37, A69, A59, RFUNCT_2:46;
then (f | X) . x in [.(((f | X) . x0) - (r / 2)),(((f | X) . x0) + (r / 2)).] by A45, A51, A68;
hence (f | X) . x in N1 by A42, A64; :: 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