theorem Th6: :: LIMFUNC2:6

for x0 being Real
for seq being Real_Sequence
for f being PartFunc of REAL,REAL st ( for n being Nat holds
( x0 < seq . n & seq . n < x0 + (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) /\ (right_open_halfline x0) )