theorem Th2: :: LIMFUNC3:2

for x0 being Real
for seq being Real_Sequence
for f being PartFunc of REAL,REAL st ( for n being Element of NAT holds
( 0 < |.(x0 - (seq . n)).| & |.(x0 - (seq . n)).| < 1 / (n + 1) & seq . n in dom f ) ) holds
( seq is convergent & lim seq = x0 & rng seq c= dom f & rng seq c= (dom f) \ {x0} )