theorem Th12: :: ASCOLI2:12

for S being non empty compact TopSpace
for T being non empty MetrSpace
for f, g being Point of (MetricSpace_of_ContinuousFunctions (S,T))
for f1, g1 being Function of S,T
for e being Real st f = f1 & g = g1 & ( for t being Point of S holds dist ((f1 . t),(g1 . t)) <= e ) holds
dist (f,g) <= e