theorem Th14: :: ASCOLI2:14

for S being non empty compact TopSpace
for T being non empty MetrSpace st T is complete holds
for H being non empty Subset of (MetricSpace_of_ContinuousFunctions (S,T)) holds
( Cl H is sequentially_compact iff (MetricSpace_of_ContinuousFunctions (S,T)) | H is totally_bounded )