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 A1: ( f is_continuous_in x0 & 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 A2: 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 ) )
assume A3: 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
consider p being real number such that
A4: ( 0 < p & N = ].(x0 - p),(x0 + p).[ ) by RCOMP_1:def 7;
A5: p is Real by XREAL_0:def 1;
deffunc H₁( Element of NAT ) -> Element of REAL = x0 - (p / ($1 + 1));
consider a being Real_Sequence such that
A6: 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
A7: for n being Element of NAT holds b . n = H₂(n) from SEQ_1:sch 1();
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 );
A8: 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]
A9: 0 <= n by NAT_1:2;
then 0 < n + 1 ;
then 0 < p / (n + 1) by A4, XREAL_1:141;
then reconsider Nn = ].(x0 - (p / (n + 1))),(x0 + (p / (n + 1))).[ as Neighbourhood of x0 by RCOMP_1:def 7;
A10: 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
A11: ( g2 = x & x0 - (p / (n + 1)) < g2 & g2 < x0 + (p / (n + 1)) ) ;
0 + 1 <= n + 1 by A9, XREAL_1:9;
then A12: p / (n + 1) <= p / 1 by A4, XREAL_1:120;
then x0 - p <= x0 - (p / (n + 1)) by XREAL_1:15;
then A13: x0 - p < g2 by A11, XXREAL_0:2;
x0 + (p / (n + 1)) <= x0 + p by A12, XREAL_1:9;
then g2 < x0 + p by A11, XXREAL_0:2;
then x in N by A4, A11, A13;
hence x in dom f by A2; :: thesis: verum

end;

then consider g being Real such that
A14: ( g in Nn & f . g = r ) by A3;
take g ; :: thesis: S₁[n,g]
ex g1 being Real st
( g1 = g & x0 - (p / (n + 1)) < g1 & g1 < x0 + (p / (n + 1)) ) by A14;
hence ( x0 - (p / (n + 1)) < g & g < x0 + (p / (n + 1)) ) ; :: thesis: ( f . g = r & g in dom f )
thus f . g = r by A14; :: thesis: g in dom f
thus g in dom f by A10, A14; :: thesis: verum

end;

consider d being Real_Sequence such that
A15: for n being Element of NAT holds S₁[n,d . n] from FUNCT_2:sch 3(A8);
A16: ( a is convergent & lim a = x0 ) by A5, A6, Th13;
A17: ( b is convergent & lim b = x0 ) by A5, A7, Th14;

A18: 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 A15;
hence ( a . n <= d . n & d . n <= b . n ) by A6, A7; :: thesis: verum

end;

then A19: d is convergent by A16, A17, SEQ_2:33;
A20: lim d = x0 by A16, A17, A18, SEQ_2:34;
A21: 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 A15; :: thesis: verum

end;

then A22: ( f /* d is convergent & f . x0 = lim (f /* d) ) by A1, A19, A20, FCONT_1:def 1;

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 A23: 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 A21, FUNCT_2:185
.= abs (r - r) by A15
.= 0 by ABSVALUE:7 ;
hence abs (((f /* d) . m) - r) < r2 by A23; :: thesis: verum

end;

hence contradiction by A1, A22, SEQ_2:def 7; :: thesis: verum