for x0 being Real
for seq being Real_Sequence
for f being PartFunc of REAL,REAL st ( rng seq c= (dom f) /\ (left_open_halfline x0) or rng seq c= (dom f) /\ (right_open_halfline x0) ) holds
rng seq c= (dom f) \ {x0}