theorem :: ASCOLI2:21

for M being non empty MetrSpace
for S being non empty compact TopSpace
for T being non empty MetrSpace
for U being compact Subset of (TopSpaceMetr T)
for F being non empty Subset of (MetricSpace_of_ContinuousFunctions (S,T))
for G being Subset of (Funcs ( the carrier of M, the carrier of T)) st S = TopSpaceMetr M & T is complete & G = F & ( for f being Function st f in F holds
rng f c= U ) holds
( (MetricSpace_of_ContinuousFunctions (S,T)) | (Cl F) is compact iff G is equicontinuous )