let x0 be Real; :: thesis:
let f be PartFunc of REAL,REAL; :: thesis:
assume that
A1: f is_convergent_in x0 and
A2: lim (f,x0) <> 0 and
A3: 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 & f . g1 <> 0 & f . g2 <> 0 ) ; :: thesis:
A4: (dom f) \ (f " {0}) = dom (f ^) by RFUNCT_1:def 2;

A5: now :: thesis:

let seq be Real_Sequence; :: thesis:
assume that
A6: seq is convergent and
A7: lim seq = x0 and
A8: rng seq c= (dom (f ^)) \ {x0} ; :: thesis:
A9: f /* seq is non-zero by A8, RFUNCT_2:11, XBOOLE_1:1;
rng seq c= dom (f ^) by A8, XBOOLE_1:1;
then A10: rng seq c= dom f by A4, XBOOLE_1:1;

let x be object ; :: thesis:
assume A11: x in rng seq ; :: thesis:
then not x in {x0} by A8, XBOOLE_0:def 5;
hence x in (dom f) \ {x0} by A10, A11, XBOOLE_0:def 5; :: thesis:

end;

then A12: rng seq c= (dom f) \ {x0} ;
then A13: lim (f /* seq) = lim (f,x0) by A1, A6, A7, Def4;
A14: (f /* seq) " = (f ^) /* seq by A8, RFUNCT_2:12, XBOOLE_1:1;
A15: f /* seq is convergent by A1, A6, A7, A12;
hence (f ^) /* seq is convergent by A2, A13, A9, A14, SEQ_2:21; :: thesis:
thus lim ((f ^) /* seq) = (lim (f,x0)) " by A2, A15, A13, A9, A14, SEQ_2:22; :: thesis:

end;

let r1, r2 be Real; :: thesis:
assume that
A16: r1 < x0 and
A17: x0 < r2 ; :: thesis:
consider g1, g2 being Real such that
A18: r1 < g1 and
A19: g1 < x0 and
A20: g1 in dom f and
A21: g2 < r2 and
A22: x0 < g2 and
A23: g2 in dom f and
A24: f . g1 <> 0 and
A25: f . g2 <> 0 by A3, A16, A17;
take g1 = g1; :: thesis:
take g2 = g2; :: thesis:
not f . g2 in {0} by A25, TARSKI:def 1;
then A26: not g2 in f " {0} by FUNCT_1:def 7;
not f . g1 in {0} by A24, TARSKI:def 1;
then not g1 in f " {0} by FUNCT_1:def 7;
hence ( r1 < g1 & g1 < x0 & g1 in dom (f ^) & g2 < r2 & x0 < g2 & g2 in dom (f ^) ) by A4, A18, A19, A20, A21, A22, A23, A26, XBOOLE_0:def 5; :: thesis:

end;

hence f ^ is_convergent_in x0 by A5; :: thesis:
hence lim ((f ^),x0) = (lim (f,x0)) " by A5, Def4; :: thesis: