for f being PartFunc of REAL,REAL
for x0 being Real st ( f is_right_convergent_in x0 or f is_right_divergent_to+infty_in x0 or f is_right_divergent_to-infty_in x0 ) holds
ex seq being Real_Sequence st
( seq is convergent & lim seq = x0 & rng seq c= (dom f) /\ (right_open_halfline x0) )