theorem Th11: :: ASCOLI2:11

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 t being Point of S holds dist ((In ((f . t),T)),(In ((g . t),T))) <= dist (f,g)