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 S₁[ 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 S₁[n,g]

proof

let n be Element of NAT ; :: thesis: ex g being Element of 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 6, XREAL_1:139;
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 A8, XREAL_1:7;
then A13: p / (n + 1) <= p / 1 by A4, XREAL_1:118;
then x0 + (p / (n + 1)) <= x0 + p by XREAL_1:7;
then A14: g2 < x0 + p by A12, XXREAL_0:2;
x0 - p <= x0 - (p / (n + 1)) by A13, XREAL_1:13;
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;
reconsider g = g as Element of REAL by XREAL_0:def 1;
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 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 A18, FUNCT_2:108, A21
.= |.(r - r).| by A17, A21
.= 0 by ABSVALUE:2 ;
hence |.(((f /* d) . m) - r).| < r2 by A20; :: thesis: verum

end;

deffunc H₁( Nat) -> set = x0 - (p / ($1 + 1));
consider a being Real_Sequence such that
A22: for n being Nat holds a . n = H₁(n) from SEQ_1:sch 1();
deffunc H₂( Nat) -> set = x0 + (p / ($1 + 1));
consider b being Real_Sequence such that
A23: for n being Nat holds b . n = H₂(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 A22, A23; :: thesis: verum

end;

A25: ( b is convergent & lim b = x0 ) by A23, Th6;
( a is convergent & lim a = x0 ) by A22, Th5;
then ( d is convergent & lim d = x0 ) by A25, A24, SEQ_2:19, SEQ_2:20;
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