defpred S1[ Element of NAT , Real] means ( x0 - (1 / ($1 + 1)) < $2 & $2 < x0 & $2 in dom f );
consider s being Real_Sequence such that
A7:
for n being Element of NAT holds S1[n,s . n]
from FUNCT_2:sch 3(A2);
A8:
rng s c= (dom f) \ {x0}
by A7, Th6;
A9:
lim s = x0
by A7, Th6;
let g1, g2 be Real; ( ( 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) = g1 ) ) & ( 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) = g2 ) ) implies g1 = g2 )
assume that
A10:
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) = g1 )
and
A11:
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) = g2 )
; g1 = g2
A12:
s is convergent
by A7, Th6;
then
lim (f /* s) = g1
by A9, A8, A10;
hence
g1 = g2
by A12, A9, A8, A11; verum