theorem Th1: :: INTEGR20:1

for X being set
for Y being RealNormSpace
for f being PartFunc of REAL, the carrier of Y holds
( f | X is uniformly_continuous iff for r being Real st 0 < r holds
ex s being Real st
( 0 < s & ( for x1, x2 being Real st x1 in dom (f | X) & x2 in dom (f | X) & |.(x1 - x2).| < s holds
||.((f /. x1) - (f /. x2)).|| < r ) ) )