for x0 being Real
for f being PartFunc of REAL,REAL st f is_continuous_in x0 & f . x0 <> 0 holds
f ^ is_continuous_in x0