let X be set ; :: thesis: for f being PartFunc of REAL,REAL st X c= dom f & f | X is monotone & ex p being Real st f .: X = left_closed_halfline p holds
f | X is continuous
let f be PartFunc of REAL,REAL; :: thesis: ( X c= dom f & f | X is monotone & ex p being Real st f .: X = left_closed_halfline p implies f | X is continuous )
assume that
A1: X c= dom f and
A2: f | X is monotone ; :: thesis: ( for p being Real holds not f .: X = left_closed_halfline p or f | X is continuous )
given p being Real such that A3: f .: X = left_closed_halfline p ; :: thesis: f | X is continuous
set L = left_open_halfline p;
set l = left_closed_halfline p;
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 )
A4: x0 in REAL by XREAL_0:def 1;
A5: (f | X) .: X = f .: X by RELAT_1:129;
A6: left_open_halfline p c= left_closed_halfline p by XXREAL_1:21;
assume x0 in dom (f | X) ; :: thesis: f | X is_continuous_in x0
then x0 in X ;
then x0 in (dom f) /\ X by A1, XBOOLE_0:def 4;
then A7: x0 in dom (f | X) by RELAT_1:61;
then (f | X) . x0 in (f | X) .: X by FUNCT_1:def 6;
then (f | X) . x0 in {p} \/ (left_open_halfline p) by A3, A5, XXREAL_1:423;
then A8: ( (f | X) . x0 in {p} or (f | X) . x0 in left_open_halfline p ) by XBOOLE_0:def 3;

now :: thesis: for N1 being Neighbourhood of (f | X) . x0 ex N being Neighbourhood of x0 st
for r1 being real number st r1 in dom (f | X) & r1 in N holds
(f | X) . r1 in N1

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

now :: thesis: ex N being Neighbourhood of x0 st
for r1 being real number st r1 in dom (f | X) & r1 in N holds
(f | X) . r1 in N1

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

suppose f | X is non-decreasing ; :: thesis: ex N being Neighbourhood of x0 st
for r1 being real number st r1 in dom (f | X) & r1 in N holds
(f | X) . r1 in N1

then A9: (f | X) | X is non-decreasing ;

now :: 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

per cases ( (f | X) . x0 in left_open_halfline p or (f | X) . x0 = p ) by A8, TARSKI:def 1;

suppose (f | X) . x0 in left_open_halfline p ; :: 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

then consider N2 being Neighbourhood of (f | X) . x0 such that
A10: N2 c= left_open_halfline p by RCOMP_1:18;
consider N3 being Neighbourhood of (f | X) . x0 such that
A11: N3 c= N1 and
A12: N3 c= N2 by RCOMP_1:17;
consider r being real number such that
A13: r > 0 and
A14: N3 = ].(((f | X) . x0) - r),(((f | X) . x0) + r).[ by RCOMP_1:def 6;
reconsider r = r as Real by XREAL_0:def 1;
A15: ((f | X) . x0) + (r / 2) < (((f | X) . x0) + (r / 2)) + (r / 2) by A13, XREAL_1:29, XREAL_1:215;
set M2 = ((f | X) . x0) + (r / 2);
A16: (f | X) . x0 < ((f | X) . x0) + (r / 2) by A13, XREAL_1:29, XREAL_1:215;
A17: (f | X) . x0 < ((f | X) . x0) + r by A13, 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 A16, XXREAL_0:2;
then A18: ((f | X) . x0) + (r / 2) in ].(((f | X) . x0) - r),(((f | X) . x0) + r).[ by A15;
then ((f | X) . x0) + (r / 2) in N2 by A12, A14;
then ((f | X) . x0) + (r / 2) in left_open_halfline p by A10;
then consider r2 being Real such that
A19: ( r2 in dom (f | X) & r2 in X ) and
A20: ((f | X) . x0) + (r / 2) = (f | X) . r2 by A3, A5, A6, PARTFUN2:59;
A21: ((f | X) . x0) + (r / 2) > (f | X) . x0 by A13, XREAL_1:29, XREAL_1:215;

A22: now :: thesis: not r2 < x0

assume A23: r2 < x0 ; :: thesis: contradiction
( x0 in X /\ (dom (f | X)) & r2 in X /\ (dom (f | X)) ) by A7, A19, XBOOLE_0:def 4;
hence contradiction by A9, A20, A21, A23, RFUNCT_2:22, A4; :: thesis: verum

end;

set M1 = ((f | X) . x0) - (r / 2);
A24: ((f | X) . x0) - r < (((f | X) . x0) - r) + (r / 2) by A13, XREAL_1:29, XREAL_1:215;
((f | X) . x0) - (r / 2) < (f | X) . x0 by A16, XREAL_1:19;
then ((f | X) . x0) - (r / 2) < ((f | X) . x0) + r by A17, XXREAL_0:2;
then A25: ((f | X) . x0) - (r / 2) in ].(((f | X) . x0) - r),(((f | X) . x0) + r).[ by A24;
then ((f | X) . x0) - (r / 2) in N2 by A12, A14;
then ((f | X) . x0) - (r / 2) in left_open_halfline p by A10;
then consider r1 being Real such that
A26: ( r1 in dom (f | X) & r1 in X ) and
A27: ((f | X) . x0) - (r / 2) = (f | X) . r1 by A3, A5, A6, PARTFUN2:59;
A28: (f | X) . x0 < ((f | X) . x0) + (r / 2) by A13, 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 < r1

assume A31: x0 < r1 ; :: thesis: contradiction
( x0 in X /\ (dom (f | X)) & r1 in X /\ (dom (f | X)) ) by A7, A26, XBOOLE_0:def 4;
hence contradiction by A9, A27, A29, A31, RFUNCT_2:22, A4; :: thesis: verum

end;

x0 <> r2 by A13, A20, XREAL_1:29, XREAL_1:215;
then x0 < r2 by A22, XXREAL_0:1;
then A32: r2 - x0 > 0 by XREAL_1:50;
set R = min ((x0 - r1),(r2 - x0));
A33: min ((x0 - r1),(r2 - x0)) <= r2 - x0 by XXREAL_0:17;
r1 <> x0 by A27, A28, XREAL_1:19;
then r1 < x0 by A30, XXREAL_0:1;
then x0 - r1 > 0 by XREAL_1:50;
then min ((x0 - r1),(r2 - x0)) > 0 by A32, 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 6;
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 )
A34: x in REAL by XREAL_0:def 1;
assume that
A35: x in dom (f | X) and
A36: x in N ; :: thesis: (f | X) . x in N1
A37: x in X /\ (dom (f | X)) by A35, XBOOLE_1:28;
A38: ex s being Real st
( s = x & x0 - (min ((x0 - r1),(r2 - x0))) < s & s < x0 + (min ((x0 - r1),(r2 - x0))) ) by A36;
then x0 < (min ((x0 - r1),(r2 - x0))) + x by XREAL_1:19;
then A39: x0 - x < ((min ((x0 - r1),(r2 - x0))) + x) - x by XREAL_1:9;
min ((x0 - r1),(r2 - x0)) <= x0 - r1 by XXREAL_0:17;
then x0 - x < x0 - r1 by A39, XXREAL_0:2;
then - (x0 - x) > - (x0 - r1) by XREAL_1:24;
then A40: (x - x0) + x0 > (r1 - x0) + x0 by XREAL_1:6;
r1 in X /\ (dom (f | X)) by A26, XBOOLE_0:def 4;
then A41: (f | X) . r1 <= (f | X) . x by A9, A40, A37, RFUNCT_2:22, A34;
x - x0 < min ((x0 - r1),(r2 - x0)) by A38, XREAL_1:19;
then x - x0 < r2 - x0 by A33, XXREAL_0:2;
then A42: (x - x0) + x0 < (r2 - x0) + x0 by XREAL_1:6;
r2 in X /\ (dom (f | X)) by A19, XBOOLE_0:def 4;
then (f | X) . x <= (f | X) . r2 by A9, A42, A37, RFUNCT_2:22, A34;
then A43: (f | X) . x in [.(((f | X) . x0) - (r / 2)),(((f | X) . x0) + (r / 2)).] by A27, A20, A41;
[.(((f | X) . x0) - (r / 2)),(((f | X) . x0) + (r / 2)).] c= ].(((f | X) . x0) - r),(((f | X) . x0) + r).[ by A25, A18, XXREAL_2:def 12;
then (f | X) . x in N3 by A14, A43;
hence (f | X) . x in N1 by A11; :: thesis: verum

end;

suppose A44: (f | X) . x0 = p ; :: 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

then consider r being real number such that
A45: r > 0 and
A46: N1 = ].(p - r),(p + r).[ by RCOMP_1:def 6;
reconsider r = r as Real by XREAL_0:def 1;
set R = r / 2;
A47: p < p + (r / 2) by A45, XREAL_1:29, XREAL_1:215;
A48: p - (r / 2) < p by A45, XREAL_1:44, XREAL_1:215;
then p - (r / 2) in { s where s is Real : s < p } ;
then p - (r / 2) in left_open_halfline p by XXREAL_1:229;
then consider r1 being Real such that
A49: ( r1 in dom (f | X) & r1 in X ) and
A50: p - (r / 2) = (f | X) . r1 by A3, A5, A6, PARTFUN2:59;
A51: r1 in X /\ (dom (f | X)) by A49, XBOOLE_0:def 4;

A52: now :: thesis: not x0 < r1

assume A53: x0 < r1 ; :: thesis: contradiction
( x0 in X /\ (dom (f | X)) & r1 in X /\ (dom (f | X)) ) by A7, A49, XBOOLE_0:def 4;
hence contradiction by A9, A44, A48, A50, A53, RFUNCT_2:22, A4; :: thesis: verum

end;

r1 <> x0 by A44, A45, A50, XREAL_1:44, XREAL_1:215;
then r1 < x0 by A52, XXREAL_0:1;
then reconsider N = ].(x0 - (x0 - r1)),(x0 + (x0 - r1)).[ as Neighbourhood of x0 by RCOMP_1:def 6, XREAL_1:50;
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
A54: x in dom (f | X) and
A55: x in N ; :: thesis: (f | X) . x in N1
A56: ex s being Real st
( s = x & x0 - (x0 - r1) < s & s < x0 + (x0 - r1) ) by A55;
A57: r / 2 < r by A45, XREAL_1:216;
then A58: p - r < p - (r / 2) by XREAL_1:15;
(f | X) . x in left_closed_halfline p by A3, A5, A54, FUNCT_1:def 6;
then (f | X) . x in { s where s is Real : s <= p } by XXREAL_1:231;
then ex s being Real st
( s = (f | X) . x & s <= p ) ;
then A59: (f | X) . x <= p + (r / 2) by A47, XXREAL_0:2;
x in X /\ (dom (f | X)) by A54, XBOOLE_0:def 4;
then p - (r / 2) <= (f | X) . x by A9, A50, A51, A56, RFUNCT_2:22;
then A60: (f | X) . x in [.(p - (r / 2)),(p + (r / 2)).] by A59;
p < p + r by A45, XREAL_1:29;
then p - (r / 2) < p + r by A48, XXREAL_0:2;
then A61: p - (r / 2) in ].(p - r),(p + r).[ by A58;
A62: p + (r / 2) < p + r by A57, XREAL_1:6;
p - r < p by A45, XREAL_1:44;
then p - r < p + (r / 2) by A47, XXREAL_0:2;
then p + (r / 2) in ].(p - r),(p + r).[ by A62;
then [.(p - (r / 2)),(p + (r / 2)).] c= N1 by A46, A61, XXREAL_2:def 12;
hence (f | X) . x in N1 by A60; :: thesis: verum

end;

end;

end;

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

end;

suppose f | X is non-increasing ; :: thesis: ex N being Neighbourhood of x0 st
for r1 being real number st r1 in dom (f | X) & r1 in N holds
(f | X) . r1 in N1

then A63: (f | X) | X is non-increasing ;

now :: 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

per cases ( (f | X) . x0 in left_open_halfline p or (f | X) . x0 = p ) by A8, TARSKI:def 1;

suppose (f | X) . x0 in left_open_halfline p ; :: 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

then consider N2 being Neighbourhood of (f | X) . x0 such that
A64: N2 c= left_open_halfline p by RCOMP_1:18;
consider N3 being Neighbourhood of (f | X) . x0 such that
A65: N3 c= N1 and
A66: N3 c= N2 by RCOMP_1:17;
consider r being real number such that
A67: r > 0 and
A68: N3 = ].(((f | X) . x0) - r),(((f | X) . x0) + r).[ by RCOMP_1:def 6;
reconsider r = r as Real by XREAL_0:def 1;
A69: ((f | X) . x0) + (r / 2) < (((f | X) . x0) + (r / 2)) + (r / 2) by A67, XREAL_1:29, XREAL_1:215;
set M2 = ((f | X) . x0) + (r / 2);
A70: (f | X) . x0 < ((f | X) . x0) + (r / 2) by A67, XREAL_1:29, XREAL_1:215;
A71: (f | X) . x0 < ((f | X) . x0) + r by A67, 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 A70, XXREAL_0:2;
then A72: ((f | X) . x0) + (r / 2) in ].(((f | X) . x0) - r),(((f | X) . x0) + r).[ by A69;
then ((f | X) . x0) + (r / 2) in N2 by A66, A68;
then ((f | X) . x0) + (r / 2) in left_open_halfline p by A64;
then consider r2 being Real such that
A73: ( r2 in dom (f | X) & r2 in X ) and
A74: ((f | X) . x0) + (r / 2) = (f | X) . r2 by A3, A5, A6, PARTFUN2:59;
A75: ((f | X) . x0) + (r / 2) > (f | X) . x0 by A67, XREAL_1:29, XREAL_1:215;

A76: now :: thesis: not r2 > x0

assume A77: r2 > x0 ; :: thesis: contradiction
( x0 in X /\ (dom (f | X)) & r2 in X /\ (dom (f | X)) ) by A7, A73, XBOOLE_0:def 4;
hence contradiction by A63, A74, A75, A77, RFUNCT_2:23, A4; :: thesis: verum

end;

set M1 = ((f | X) . x0) - (r / 2);
A78: ((f | X) . x0) - r < (((f | X) . x0) - r) + (r / 2) by A67, XREAL_1:29, XREAL_1:215;
((f | X) . x0) - (r / 2) < (f | X) . x0 by A70, XREAL_1:19;
then ((f | X) . x0) - (r / 2) < ((f | X) . x0) + r by A71, XXREAL_0:2;
then A79: ((f | X) . x0) - (r / 2) in ].(((f | X) . x0) - r),(((f | X) . x0) + r).[ by A78;
then ((f | X) . x0) - (r / 2) in N2 by A66, A68;
then ((f | X) . x0) - (r / 2) in left_open_halfline p by A64;
then consider r1 being Real such that
A80: ( r1 in dom (f | X) & r1 in X ) and
A81: ((f | X) . x0) - (r / 2) = (f | X) . r1 by A3, A5, A6, PARTFUN2:59;
A82: (f | X) . x0 < ((f | X) . x0) + (r / 2) by A67, XREAL_1:29, XREAL_1:215;
then A83: ((f | X) . x0) - (r / 2) < (f | X) . x0 by XREAL_1:19;

A84: now :: thesis: not x0 > r1

assume A85: x0 > r1 ; :: thesis: contradiction
( x0 in X /\ (dom (f | X)) & r1 in X /\ (dom (f | X)) ) by A7, A80, XBOOLE_0:def 4;
hence contradiction by A63, A81, A83, A85, RFUNCT_2:23, A4; :: thesis: verum

end;

x0 <> r2 by A67, A74, XREAL_1:29, XREAL_1:215;
then x0 > r2 by A76, XXREAL_0:1;
then A86: x0 - r2 > 0 by XREAL_1:50;
set R = min ((r1 - x0),(x0 - r2));
A87: min ((r1 - x0),(x0 - r2)) <= r1 - x0 by XXREAL_0:17;
r1 <> x0 by A81, A82, XREAL_1:19;
then r1 > x0 by A84, XXREAL_0:1;
then r1 - x0 > 0 by XREAL_1:50;
then min ((r1 - x0),(x0 - r2)) > 0 by A86, 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 6;
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 )
A88: x in REAL by XREAL_0:def 1;
assume that
A89: x in dom (f | X) and
A90: x in N ; :: thesis: (f | X) . x in N1
A91: x in X /\ (dom (f | X)) by A89, XBOOLE_1:28;
A92: ex s being Real st
( s = x & x0 - (min ((r1 - x0),(x0 - r2))) < s & s < x0 + (min ((r1 - x0),(x0 - r2))) ) by A90;
then x0 < (min ((r1 - x0),(x0 - r2))) + x by XREAL_1:19;
then A93: x0 - x < ((min ((r1 - x0),(x0 - r2))) + x) - x by XREAL_1:9;
x - x0 < min ((r1 - x0),(x0 - r2)) by A92, XREAL_1:19;
then x - x0 < r1 - x0 by A87, XXREAL_0:2;
then A94: (x - x0) + x0 < (r1 - x0) + x0 by XREAL_1:6;
r1 in X /\ (dom (f | X)) by A80, XBOOLE_0:def 4;
then A95: (f | X) . r1 <= (f | X) . x by A63, A94, A91, RFUNCT_2:23, A88;
min ((r1 - x0),(x0 - r2)) <= x0 - r2 by XXREAL_0:17;
then x0 - x < x0 - r2 by A93, XXREAL_0:2;
then - (x0 - x) > - (x0 - r2) by XREAL_1:24;
then A96: (x - x0) + x0 > (r2 - x0) + x0 by XREAL_1:6;
r2 in X /\ (dom (f | X)) by A73, XBOOLE_0:def 4;
then (f | X) . x <= (f | X) . r2 by A63, A96, A91, RFUNCT_2:23, A88;
then A97: (f | X) . x in [.(((f | X) . x0) - (r / 2)),(((f | X) . x0) + (r / 2)).] by A81, A74, A95;
[.(((f | X) . x0) - (r / 2)),(((f | X) . x0) + (r / 2)).] c= ].(((f | X) . x0) - r),(((f | X) . x0) + r).[ by A79, A72, XXREAL_2:def 12;
then (f | X) . x in N3 by A68, A97;
hence (f | X) . x in N1 by A65; :: thesis: verum

end;

suppose A98: (f | X) . x0 = p ; :: 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

then consider r being real number such that
A99: r > 0 and
A100: N1 = ].(p - r),(p + r).[ by RCOMP_1:def 6;
reconsider r = r as Real by XREAL_0:def 1;
set R = r / 2;
A101: p < p + (r / 2) by A99, XREAL_1:29, XREAL_1:215;
A102: p - (r / 2) < p by A99, XREAL_1:44, XREAL_1:215;
then p - (r / 2) in { s where s is Real : s < p } ;
then p - (r / 2) in left_open_halfline p by XXREAL_1:229;
then consider r1 being Real such that
A103: ( r1 in dom (f | X) & r1 in X ) and
A104: p - (r / 2) = (f | X) . r1 by A3, A5, A6, PARTFUN2:59;
A105: r1 in X /\ (dom (f | X)) by A103, XBOOLE_0:def 4;

A106: now :: thesis: not x0 > r1

assume A107: x0 > r1 ; :: thesis: contradiction
( x0 in X /\ (dom (f | X)) & r1 in X /\ (dom (f | X)) ) by A7, A103, XBOOLE_0:def 4;
hence contradiction by A63, A98, A102, A104, A107, RFUNCT_2:23, A4; :: thesis: verum

end;

r1 <> x0 by A98, A99, A104, XREAL_1:44, XREAL_1:215;
then r1 > x0 by A106, XXREAL_0:1;
then reconsider N = ].(x0 - (r1 - x0)),(x0 + (r1 - x0)).[ as Neighbourhood of x0 by RCOMP_1:def 6, XREAL_1:50;
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
A108: x in dom (f | X) and
A109: x in N ; :: thesis: (f | X) . x in N1
A110: ex s being Real st
( s = x & x0 - (r1 - x0) < s & s < x0 + (r1 - x0) ) by A109;
A111: r / 2 < r by A99, XREAL_1:216;
then A112: p - r < p - (r / 2) by XREAL_1:15;
(f | X) . x in left_closed_halfline p by A3, A5, A108, FUNCT_1:def 6;
then (f | X) . x in { s where s is Real : s <= p } by XXREAL_1:231;
then ex s being Real st
( s = (f | X) . x & s <= p ) ;
then A113: (f | X) . x <= p + (r / 2) by A101, XXREAL_0:2;
x in X /\ (dom (f | X)) by A108, XBOOLE_0:def 4;
then p - (r / 2) <= (f | X) . x by A63, A104, A105, A110, RFUNCT_2:23;
then A114: (f | X) . x in [.(p - (r / 2)),(p + (r / 2)).] by A113;
p < p + r by A99, XREAL_1:29;
then p - (r / 2) < p + r by A102, XXREAL_0:2;
then A115: p - (r / 2) in ].(p - r),(p + r).[ by A112;
A116: p + (r / 2) < p + r by A111, XREAL_1:6;
p - r < p by A99, XREAL_1:44;
then p - r < p + (r / 2) by A101, XXREAL_0:2;
then p + (r / 2) in ].(p - r),(p + r).[ by A116;
then [.(p - (r / 2)),(p + (r / 2)).] c= N1 by A100, A115, XXREAL_2:def 12;
hence (f | X) . x in N1 by A114; :: thesis: verum

end;

end;

end;

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

end;

end;

end;

hence ex N being Neighbourhood of x0 st
for r1 being real number st r1 in dom (f | X) & r1 in N holds
(f | X) . r1 in N1 ; :: 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