theorem Th36: :: PDIFF_9:36

for i being Element of NAT
for f being PartFunc of (REAL i),REAL
for x0 being Element of REAL i holds
( f is_continuous_in x0 iff ( x0 in dom f & ( for r being Real st 0 < r holds
ex s being Real st
( 0 < s & ( for x being Element of REAL i st x in dom f & |.(x - x0).| < s holds
|.((f /. x) - (f /. x0)).| < r ) ) ) ) )