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_{1}[ 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_{1}[n,g]

A17: for n being Element of NAT holds S_{1}[n,d . n]
from FUNCT_2:sch 3(A7);

A18: rng d c= dom f_{1}( Nat) -> set = x0 - (p / ($1 + 1));

consider a being Real_Sequence such that

A22: for n being Nat holds a . n = H_{1}(n)
from SEQ_1:sch 1();

deffunc H_{2}( Nat) -> set = x0 + (p / ($1 + 1));

consider b being Real_Sequence such that

A23: for n being Nat holds b . n = H_{2}(n)
from SEQ_1:sch 1();

( 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

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

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

proof

consider d being Real_Sequence such that
let n be Element of NAT ; :: thesis: ex g being Element of REAL st S_{1}[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

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_{1}[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;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

then consider g being Real such that
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;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

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

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

A17: for n being Element of NAT holds S

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;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

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

deffunc Hex 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;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

consider a being Real_Sequence such that

A22: for n being Nat holds a . n = H

deffunc H

consider b being Real_Sequence such that

A23: for n being Nat holds b . n = H

A24: now :: thesis: for n being Nat holds

( a . n <= d . n & d . n <= b . n )

A25:
( b is convergent & lim b = x0 )
by A23, Th6;( 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;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

( 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