theorem Th6: :: FDIFF_3:6

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