let x0 be Real; :: thesis: for f being PartFunc of REAL,REAL holds
( f is_convergent_in x0 iff ( ( for r1, r2 being Real st r1 < x0 & x0 < r2 holds
ex g1, g2 being Real st
( r1 < g1 & g1 < x0 & g1 in dom f & g2 < r2 & x0 < g2 & g2 in dom f ) ) & ex g being Real st
for g1 being Real st 0 < g1 holds
ex g2 being Real st
( 0 < g2 & ( for r1 being Real st 0 < abs (x0 - r1) & abs (x0 - r1) < g2 & r1 in dom f holds
abs ((f . r1) - g) < g1 ) ) ) )
let f be PartFunc of REAL,REAL; :: thesis: ( f is_convergent_in x0 iff ( ( for r1, r2 being Real st r1 < x0 & x0 < r2 holds
ex g1, g2 being Real st
( r1 < g1 & g1 < x0 & g1 in dom f & g2 < r2 & x0 < g2 & g2 in dom f ) ) & ex g being Real st
for g1 being Real st 0 < g1 holds
ex g2 being Real st
( 0 < g2 & ( for r1 being Real st 0 < abs (x0 - r1) & abs (x0 - r1) < g2 & r1 in dom f holds
abs ((f . r1) - g) < g1 ) ) ) )
thus ( f is_convergent_in x0 implies ( ( for r1, r2 being Real st r1 < x0 & x0 < r2 holds
ex g1, g2 being Real st
( r1 < g1 & g1 < x0 & g1 in dom f & g2 < r2 & x0 < g2 & g2 in dom f ) ) & ex g being Real st
for g1 being Real st 0 < g1 holds
ex g2 being Real st
( 0 < g2 & ( for r1 being Real st 0 < abs (x0 - r1) & abs (x0 - r1) < g2 & r1 in dom f holds
abs ((f . r1) - g) < g1 ) ) ) ) :: thesis: ( ( for r1, r2 being Real st r1 < x0 & x0 < r2 holds
ex g1, g2 being Real st
( r1 < g1 & g1 < x0 & g1 in dom f & g2 < r2 & x0 < g2 & g2 in dom f ) ) & ex g being Real st
for g1 being Real st 0 < g1 holds
ex g2 being Real st
( 0 < g2 & ( for r1 being Real st 0 < abs (x0 - r1) & abs (x0 - r1) < g2 & r1 in dom f holds
abs ((f . r1) - g) < g1 ) ) implies f is_convergent_in x0 )

proof

assume that
A1: f is_convergent_in x0 and
A2: ( ex r1, r2 being Real st
( r1 < x0 & x0 < r2 & ( for g1, g2 being Real holds
( not r1 < g1 or not g1 < x0 or not g1 in dom f or not g2 < r2 or not x0 < g2 or not g2 in dom f ) ) ) or for g being Real ex g1 being Real st
( 0 < g1 & ( for g2 being Real st 0 < g2 holds
ex r1 being Real st
( 0 < abs (x0 - r1) & abs (x0 - r1) < g2 & r1 in dom f & abs ((f . r1) - g) >= g1 ) ) ) ) ; :: thesis: contradiction
consider g being Real such that
A3: for seq being Real_Sequence st seq is convergent & lim seq = x0 & rng seq c= (dom f) \ {x0} holds
( f /* seq is convergent & lim (f /* seq) = g ) by A1, Def1;
consider g1 being Real such that
A4: 0 < g1 and
A5: for g2 being Real st 0 < g2 holds
ex r1 being Real st
( 0 < abs (x0 - r1) & abs (x0 - r1) < g2 & r1 in dom f & abs ((f . r1) - g) >= g1 ) by A1, A2, Def1;
defpred S₁[ Element of NAT , real number ] means ( 0 < abs (x0 - $2) & abs (x0 - $2) < 1 / ($1 + 1) & $2 in dom f & abs ((f . $2) - g) >= g1 );
A6: for n being Element of NAT ex r1 being Real st S₁[n,r1] by A5, XREAL_1:139;
consider s being Real_Sequence such that
A7: for n being Element of NAT holds S₁[n,s . n] from FUNCT_2:sch 3(A6);
A8: rng s c= (dom f) \ {x0} by A7, Th2;
A9: lim s = x0 by A7, Th2;
A10: s is convergent by A7, Th2;
then A11: lim (f /* s) = g by A3, A9, A8;
f /* s is convergent by A3, A10, A9, A8;
then consider n being Element of NAT such that
A12: for k being Element of NAT st n <= k holds
abs (((f /* s) . k) - g) < g1 by A4, A11, SEQ_2:def 7;
A13: abs (((f /* s) . n) - g) < g1 by A12;
rng s c= dom f by A7, Th2;
then abs ((f . (s . n)) - g) < g1 by A13, FUNCT_2:108;
hence contradiction by A7; :: thesis: verum

end;

assume A14: for r1, r2 being Real st r1 < x0 & x0 < r2 holds
ex g1, g2 being Real st
( r1 < g1 & g1 < x0 & g1 in dom f & g2 < r2 & x0 < g2 & g2 in dom f ) ; :: thesis: ( for g being Real ex g1 being Real st
( 0 < g1 & ( for g2 being Real holds
( not 0 < g2 or ex r1 being Real st
( 0 < abs (x0 - r1) & abs (x0 - r1) < g2 & r1 in dom f & not abs ((f . r1) - g) < g1 ) ) ) ) or f is_convergent_in x0 )
given g being Real such that A15: for g1 being Real st 0 < g1 holds
ex g2 being Real st
( 0 < g2 & ( for r1 being Real st 0 < abs (x0 - r1) & abs (x0 - r1) < g2 & r1 in dom f holds
abs ((f . r1) - g) < g1 ) ) ; :: thesis: f is_convergent_in x0

now

let s be Real_Sequence; :: thesis: ( s is convergent & lim s = x0 & rng s c= (dom f) \ {x0} implies ( f /* s is convergent & lim (f /* s) = g ) )
assume that
A16: s is convergent and
A17: lim s = x0 and
A18: rng s c= (dom f) \ {x0} ; :: thesis: ( f /* s is convergent & lim (f /* s) = g )

A19: now

let g1 be real number ; :: thesis: ( 0 < g1 implies ex n being Element of NAT st
for k being Element of NAT st n <= k holds
abs (((f /* s) . k) - g) < g1 )
assume A20: 0 < g1 ; :: thesis: ex n being Element of NAT st
for k being Element of NAT st n <= k holds
abs (((f /* s) . k) - g) < g1
g1 is Real by XREAL_0:def 1;
then consider g2 being Real such that
A21: 0 < g2 and
A22: for r1 being Real st 0 < abs (x0 - r1) & abs (x0 - r1) < g2 & r1 in dom f holds
abs ((f . r1) - g) < g1 by A15, A20;
consider n being Element of NAT such that
A23: for k being Element of NAT st n <= k holds
( 0 < abs (x0 - (s . k)) & abs (x0 - (s . k)) < g2 & s . k in dom f ) by A16, A17, A18, A21, Th3;
take n = n; :: thesis: for k being Element of NAT st n <= k holds
abs (((f /* s) . k) - g) < g1
let k be Element of NAT ; :: thesis: ( n <= k implies abs (((f /* s) . k) - g) < g1 )
assume A24: n <= k ; :: thesis: abs (((f /* s) . k) - g) < g1
then A25: abs (x0 - (s . k)) < g2 by A23;
A26: s . k in dom f by A23, A24;
0 < abs (x0 - (s . k)) by A23, A24;
then abs ((f . (s . k)) - g) < g1 by A22, A25, A26;
hence abs (((f /* s) . k) - g) < g1 by A18, FUNCT_2:108, XBOOLE_1:1; :: thesis: verum

end;

hence f /* s is convergent by SEQ_2:def 6; :: thesis: lim (f /* s) = g
hence lim (f /* s) = g by A19, SEQ_2:def 7; :: thesis: verum

end;

hence f is_convergent_in x0 by A14, Def1; :: thesis: verum