theorem Th28: :: FDIFF_12:28

for x0 being Real
for f being PartFunc of REAL,REAL holds
( f is_Rcontinuous_in x0 iff ( x0 in dom f & ( for e being Real st 0 < e holds
ex d being Real st
( 0 < d & ( for x being Real st x in dom f & x0 < x & x < x0 + d holds
|.((f . x) - (f . x0)).| < e ) ) ) ) )