let g, x0 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 < |.(x0 - r1).| & |.(x0 - r1).| < g2 & r1 in dom f holds
|.((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 < |.(x0 - r1).| & |.(x0 - r1).| < g2 & r1 in dom f holds
|.((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 < |.(x0 - r1).| & |.(x0 - r1).| < g2 & r1 in dom f holds
|.((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 < |.(x0 - r1).| & |.(x0 - r1).| < g2 & r1 in dom f holds
|.((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 < |.(x0 - r1).| & |.(x0 - r1).| < g2 & r1 in dom f holds
|.((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 < |.(x0 - r1).| & |.(x0 - r1).| < g2 & r1 in dom f & g1 <= |.((f . r1) - g).| ) ) ) ; :: thesis: contradiction
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 < |.(x0 - r1).| & |.(x0 - r1).| < g2 & r1 in dom f & g1 <= |.((f . r1) - g).| ) by A3;
defpred S₁[ Element of NAT , Real] means ( 0 < |.(x0 - $2).| & |.(x0 - $2).| < 1 / ($1 + 1) & $2 in dom f & |.((f . $2) - g).| >= g1 );
A6: for n being Element of NAT ex r1 being Element of REAL st S₁[n,r1]

proof

let n be Element of NAT ; :: thesis: ex r1 being Element of REAL st S₁[n,r1]
consider r1 being Real such that
A7: S₁[n,r1] by A5, XREAL_1:139;
reconsider r1 = r1 as Element of REAL by XREAL_0:def 1;
take r1 ; :: thesis: S₁[n,r1]
thus S₁[n,r1] by A7; :: thesis: verum

end;

consider s being Real_Sequence such that
A8: for n being Element of NAT holds S₁[n,s . n] from FUNCT_2:sch 3(A6);
A9: rng s c= (dom f) \ {x0} by A8, Th2;
A10: lim s = x0 by A8, Th2;
A11: s is convergent by A8, Th2;
then A12: lim (f /* s) = g by A1, A2, A10, A9, Def4;
f /* s is convergent by A1, A11, A10, A9;
then consider n being Nat such that
A13: for k being Nat st n <= k holds
|.(((f /* s) . k) - g).| < g1 by A4, A12, SEQ_2:def 7;
A14: |.(((f /* s) . n) - g).| < g1 by A13;
A15: n in NAT by ORDINAL1:def 12;
rng s c= dom f by A8, Th2;
then |.((f . (s . n)) - g).| < g1 by A14, FUNCT_2:108, A15;
hence contradiction by A8, A15; :: thesis: verum

end;

assume A16: for g1 being Real st 0 < g1 holds
ex g2 being Real st
( 0 < g2 & ( for r1 being Real st 0 < |.(x0 - r1).| & |.(x0 - r1).| < g2 & r1 in dom f holds
|.((f . r1) - g).| < g1 ) ) ; :: thesis: lim (f,x0) = g
reconsider g = g as Real ;

now :: thesis: for s being Real_Sequence st s is convergent & lim s = x0 & rng s c= (dom f) \ {x0} holds
( f /* s is convergent & lim (f /* s) = g )

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

A20: now :: thesis: for g1 being Real st 0 < g1 holds
ex n being Nat st
for k being Nat st n <= k holds
|.(((f /* s) . k) - g).| < g1

let g1 be Real; :: thesis: ( 0 < g1 implies ex n being Nat st
for k being Nat st n <= k holds
|.(((f /* s) . k) - g).| < g1 )
assume A21: 0 < g1 ; :: thesis: ex n being Nat st
for k being Nat st n <= k holds
|.(((f /* s) . k) - g).| < g1
consider g2 being Real such that
A22: 0 < g2 and
A23: for r1 being Real st 0 < |.(x0 - r1).| & |.(x0 - r1).| < g2 & r1 in dom f holds
|.((f . r1) - g).| < g1 by A16, A21;
consider n being Element of NAT such that
A24: for k being Element of NAT st n <= k holds
( 0 < |.(x0 - (s . k)).| & |.(x0 - (s . k)).| < g2 & s . k in dom f ) by A17, A18, A19, A22, Th3;
reconsider n = n as Nat ;
take n = n; :: thesis: for k being Nat st n <= k holds
|.(((f /* s) . k) - g).| < g1
let k be Nat; :: thesis: ( n <= k implies |.(((f /* s) . k) - g).| < g1 )
A25: k in NAT by ORDINAL1:def 12;
assume A26: n <= k ; :: thesis: |.(((f /* s) . k) - g).| < g1
then A27: |.(x0 - (s . k)).| < g2 by A24, A25;
A28: s . k in dom f by A24, A26, A25;
0 < |.(x0 - (s . k)).| by A24, A26, A25;
then |.((f . (s . k)) - g).| < g1 by A23, A27, A28;
hence |.(((f /* s) . k) - g).| < g1 by A19, FUNCT_2:108, XBOOLE_1:1, A25; :: thesis: verum

end;

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

end;

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