theorem Th8: :: ASCOLI2:8

for S being non empty 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
Dist is continuous