theorem Th7: :: UNIFORM1:7

for N, M being non empty MetrSpace
for f being Function of N,M
for g being Function of (TopSpaceMetr N),(TopSpaceMetr M) st g = f & TopSpaceMetr N is compact & g is continuous holds
f is uniformly_continuous