theorem :: FDIFF_2:10

for x0, r being Real
for f being PartFunc of REAL,REAL st f . x0 <> r & f is_differentiable_in x0 holds
ex N being Neighbourhood of x0 st
( N c= dom f & ( for g being Real st g in N holds
f . g <> r ) ) by FCONT_3:7, FDIFF_1:24;