let x0, g be Real; :: thesis: for f being PartFunc of REAL ,REAL st f is_convergent_in x0 holds
( lim f,x0 = g iff 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 implies ( lim f,x0 = g iff 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 ) ) ) )
assume A1: f is_convergent_in x0 ; :: thesis: ( lim f,x0 = g iff 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 ( lim f,x0 = g implies 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 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 lim f,x0 = g )

proof

assume that
A2: lim f,x0 = g and
A3: 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 & g1 <= abs ((f . r1) - g) ) ) ) ; :: thesis: contradiction
consider g1 being Real such that
A4: ( 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 & g1 <= abs ((f . r1) - g) ) ) ) by A3;
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 );
A5: for n being Element of NAT ex r1 being Real st S₁[n,r1] by A4, XREAL_1:141;
consider s being Real_Sequence such that
A7: for n being Element of NAT holds S₁[n,s . n] from FUNCT_2:sch 3(A5);
A8: ( s is convergent & lim s = x0 & rng s c= dom f & rng s c= (dom f) \ {x0} ) by A7, Th2;
then ( f /* s is convergent & lim (f /* s) = g ) by A1, A2, Def4;
then consider n being Element of NAT such that
A9: for k being Element of NAT st n <= k holds
abs (((f /* s) . k) - g) < g1 by A4, SEQ_2:def 7;
abs (((f /* s) . n) - g) < g1 by A9;
then abs ((f . (s . n)) - g) < g1 by A8, FUNCT_2:185;
hence contradiction by A7; :: thesis: verum

end;

assume A10: 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: lim f,x0 = g

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 A11: ( s is convergent & lim s = x0 & rng s c= (dom f) \ {x0} ) ; :: thesis: ( f /* s is convergent & lim (f /* s) = g )

A12: 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 )
A13: g1 is Real by XREAL_0:def 1;
assume 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
then consider g2 being Real such that
A14: ( 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 ) ) by A10, A13;
consider n being Element of NAT such that
A15: 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 A11, A14, 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 n <= k ; :: thesis: abs (((f /* s) . k) - g) < g1
then ( 0 < abs (x0 - (s . k)) & abs (x0 - (s . k)) < g2 & s . k in dom f ) by A15;
then abs ((f . (s . k)) - g) < g1 by A14;
hence abs (((f /* s) . k) - g) < g1 by A11, FUNCT_2:185, 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 A12, SEQ_2:def 7; :: thesis: verum

end;

hence lim f,x0 = g by A1, Def4; :: thesis: verum