let x0, r be Real; :: thesis: for f being PartFunc of REAL,REAL st f is_continuous_in x0 & f . x0 <> r & ex N being Neighbourhood of x0 st N c= dom f holds
ex N being Neighbourhood of x0 st
( N c= dom f & ( for g being Real st g in N holds
f . g <> r ) )

let f be PartFunc of REAL,REAL; :: thesis: ( f is_continuous_in x0 & f . x0 <> r & ex N being Neighbourhood of x0 st N c= dom f implies ex N being Neighbourhood of x0 st
( N c= dom f & ( for g being Real st g in N holds
f . g <> r ) ) )

assume that
A1: f is_continuous_in x0 and
A2: f . x0 <> r ; :: thesis: ( for N being Neighbourhood of x0 holds not N c= dom f or ex N being Neighbourhood of x0 st
( N c= dom f & ( for g being Real st g in N holds
f . g <> r ) ) )

given N being Neighbourhood of x0 such that A3: N c= dom f ; :: thesis: ex N being Neighbourhood of x0 st
( N c= dom f & ( for g being Real st g in N holds
f . g <> r ) )

consider p being Real such that
A4: 0 < p and
A5: N = ].(x0 - p),(x0 + p).[ by RCOMP_1:def 6;
defpred S1[ Nat, Real] means ( x0 - (p / (\$1 + 1)) < \$2 & \$2 < x0 + (p / (\$1 + 1)) & f . \$2 = r & \$2 in dom f );
assume A6: for N being Neighbourhood of x0 holds
( not N c= dom f or ex g being Real st
( g in N & f . g = r ) ) ; :: thesis: contradiction
A7: for n being Element of NAT ex g being Element of REAL st S1[n,g]
proof
let n be Element of NAT ; :: thesis: ex g being Element of REAL st S1[n,g]
A8: 0 <= n by NAT_1:2;
then reconsider Nn = ].(x0 - (p / (n + 1))),(x0 + (p / (n + 1))).[ as Neighbourhood of x0 by ;
A9: Nn c= dom f
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Nn or x in dom f )
assume x in Nn ; :: thesis: x in dom f
then consider g2 being Real such that
A10: g2 = x and
A11: x0 - (p / (n + 1)) < g2 and
A12: g2 < x0 + (p / (n + 1)) ;
0 + 1 <= n + 1 by ;
then A13: p / (n + 1) <= p / 1 by ;
then x0 + (p / (n + 1)) <= x0 + p by XREAL_1:7;
then A14: g2 < x0 + p by ;
x0 - p <= x0 - (p / (n + 1)) by ;
then x0 - p < g2 by ;
then x in N by A5, A10, A14;
hence x in dom f by A3; :: thesis: verum
end;
then consider g being Real such that
A15: g in Nn and
A16: f . g = r by A6;
reconsider g = g as Element of REAL by XREAL_0:def 1;
take g ; :: thesis: S1[n,g]
ex g1 being Real st
( g1 = g & x0 - (p / (n + 1)) < g1 & g1 < x0 + (p / (n + 1)) ) by A15;
hence ( x0 - (p / (n + 1)) < g & g < x0 + (p / (n + 1)) ) ; :: thesis: ( f . g = r & g in dom f )
thus f . g = r by A16; :: thesis: g in dom f
thus g in dom f by ; :: thesis: verum
end;
consider d being Real_Sequence such that
A17: for n being Element of NAT holds S1[n,d . n] from A18: rng d c= dom f
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng d or x in dom f )
assume x in rng d ; :: thesis: x in dom f
then ex n being Element of NAT st x = d . n by FUNCT_2:113;
hence x in dom f by A17; :: thesis: verum
end;
A19: now :: thesis: for r2 being Real st 0 < r2 holds
ex n being Nat st
for m being Nat st n <= m holds
|.(((f /* d) . m) - r).| < r2
let r2 be Real; :: thesis: ( 0 < r2 implies ex n being Nat st
for m being Nat st n <= m holds
|.(((f /* d) . m) - r).| < r2 )

assume A20: 0 < r2 ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
|.(((f /* d) . m) - r).| < r2

reconsider n = 0 as Nat ;
take n = n; :: thesis: for m being Nat st n <= m holds
|.(((f /* d) . m) - r).| < r2

let m be Nat; :: thesis: ( n <= m implies |.(((f /* d) . m) - r).| < r2 )
assume n <= m ; :: thesis: |.(((f /* d) . m) - r).| < r2
A21: m in NAT by ORDINAL1:def 12;
|.(((f /* d) . m) - r).| = |.((f . (d . m)) - r).| by
.= |.(r - r).| by
.= 0 by ABSVALUE:2 ;
hence |.(((f /* d) . m) - r).| < r2 by A20; :: thesis: verum
end;
deffunc H1( Nat) -> set = x0 - (p / (\$1 + 1));
consider a being Real_Sequence such that
A22: for n being Nat holds a . n = H1(n) from SEQ_1:sch 1();
deffunc H2( Nat) -> set = x0 + (p / (\$1 + 1));
consider b being Real_Sequence such that
A23: for n being Nat holds b . n = H2(n) from SEQ_1:sch 1();
A24: now :: thesis: for n being Nat holds
( a . n <= d . n & d . n <= b . n )
let n be Nat; :: thesis: ( a . n <= d . n & d . n <= b . n )
n in NAT by ORDINAL1:def 12;
then ( x0 - (p / (n + 1)) < d . n & d . n < x0 + (p / (n + 1)) ) by A17;
hence ( a . n <= d . n & d . n <= b . n ) by ; :: thesis: verum
end;
A25: ( b is convergent & lim b = x0 ) by ;
( a is convergent & lim a = x0 ) by ;
then ( d is convergent & lim d = x0 ) by ;
then ( f /* d is convergent & f . x0 = lim (f /* d) ) by ;
hence contradiction by A2, A19, SEQ_2:def 7; :: thesis: verum