theorem Th9: :: ASCOLI2:9

for S being non empty compact TopSpace
for T being non empty MetrSpace
for f, g being Function of S,(TopSpaceMetr T) st f is continuous & g is continuous holds
for Dist being RealMap of S st ( for x being Point of S holds Dist . x = dist ((In ((f . x),T)),(In ((g . x),T))) ) holds
( rng Dist <> {} & rng Dist is bounded_above & rng Dist is bounded_below )