let x0 be Real; :: thesis: for r being real number
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 r be real number ; :: 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 number such that
A4: 0 < p and
A5: N = ].(x0 - p),(x0 + p).[ by RCOMP_1:def 7;
defpred S₁[ Element of NAT , real number ] 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 Real st S₁[n,g]

proof

let n be Element of NAT ; :: thesis: ex g being Real st S₁[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 A4, RCOMP_1:def 7, XREAL_1:141;
A9: Nn c= dom f

proof

let x be set ; :: 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 A8, XREAL_1:9;
then A13: p / (n + 1) <= p / 1 by A4, XREAL_1:120;
then x0 + (p / (n + 1)) <= x0 + p by XREAL_1:9;
then A14: g2 < x0 + p by A12, XXREAL_0:2;
x0 - p <= x0 - (p / (n + 1)) by A13, XREAL_1:15;
then x0 - p < g2 by A11, XXREAL_0:2;
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;
take g ; :: thesis: S₁[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 A9, A15; :: thesis: verum

end;

consider d being Real_Sequence such that
A17: for n being Element of NAT holds S₁[n,d . n] from FUNCT_2:sch 3(A7);
A18: rng d c= dom f

proof

let x be set ; :: 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:190;
hence x in dom f by A17; :: thesis: verum

end;

A19: now

let r2 be real number ; :: thesis: ( 0 < r2 implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs (((f /* d) . m) - r) < r2 )
assume A20: 0 < r2 ; :: thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs (((f /* d) . m) - r) < r2
take n = 0 ; :: thesis: for m being Element of NAT st n <= m holds
abs (((f /* d) . m) - r) < r2
let m be Element of NAT ; :: thesis: ( n <= m implies abs (((f /* d) . m) - r) < r2 )
assume n <= m ; :: thesis: abs (((f /* d) . m) - r) < r2
abs (((f /* d) . m) - r) = abs ((f . (d . m)) - r) by A18, FUNCT_2:185
.= abs (r - r) by A17
.= 0 by ABSVALUE:7 ;
hence abs (((f /* d) . m) - r) < r2 by A20; :: thesis: verum

end;

deffunc H₁( Element of NAT ) -> Element of REAL = x0 - (p / ($1 + 1));
consider a being Real_Sequence such that
A21: for n being Element of NAT holds a . n = H₁(n) from SEQ_1:sch 1();
deffunc H₂( Element of NAT ) -> Element of REAL = x0 + (p / ($1 + 1));
consider b being Real_Sequence such that
A22: for n being Element of NAT holds b . n = H₂(n) from SEQ_1:sch 1();

A23: now

let n be Element of NAT ; :: thesis: ( a . n <= d . n & d . n <= b . n )
( x0 - (p / (n + 1)) < d . n & d . n < x0 + (p / (n + 1)) ) by A17;
hence ( a . n <= d . n & d . n <= b . n ) by A21, A22; :: thesis: verum

end;

A24: p is Real by XREAL_0:def 1;
then A25: ( b is convergent & lim b = x0 ) by A22, Th14;
( a is convergent & lim a = x0 ) by A24, A21, Th13;
then ( d is convergent & lim d = x0 ) by A25, A23, SEQ_2:33, SEQ_2:34;
then ( f /* d is convergent & f . x0 = lim (f /* d) ) by A1, A18, FCONT_1:def 1;
hence contradiction by A2, A19, SEQ_2:def 7; :: thesis: verum