theorem Th8: :: FDIFF_3:8

for f being PartFunc of REAL,REAL
for x0, g2 being Real st f is_Rcontinuous_in x0 & f . x0 <> g2 & ex r being Real st
( r > 0 & [.x0,(x0 + r).] c= dom f ) holds
ex r1 being Real st
( r1 > 0 & [.x0,(x0 + r1).] c= dom f & ( for g being Real st g in [.x0,(x0 + r1).] holds
f . g <> g2 ) )