theorem Th13: :: ASCOLI2:13

for S being non empty compact TopSpace
for T being non empty MetrSpace st T is complete holds
MetricSpace_of_ContinuousFunctions (S,T) is complete