theorem Th80a: :: DUALSP05:3

for X being non empty strict SubSpace of R^1
for f being RealMap of X
for g being PartFunc of REAL,REAL
for x being Point of X
for x0 being Real st g = f & x = x0 holds
( ( for V being Subset of REAL st f . x in V & V is open holds
ex W being Subset of X st
( x in W & W is open & f .: W c= V ) ) iff g is_continuous_in x0 )