theorem Th5: :: ASCOLI:5

for S being non empty MetrSpace
for T being RealNormSpace
for F being Subset of (Funcs ( the carrier of S, the carrier of T)) st TopSpaceMetr S is compact holds
( F is equicontinuous iff for x being Point of S holds F is_equicontinuous_at x )