theorem Th17: :: ASCOLI2:17

for M being non empty MetrSpace
for S being non empty compact TopSpace
for T being non empty MetrSpace
for G being Subset of (Funcs ( the carrier of M, the carrier of T))
for H being non empty Subset of (MetricSpace_of_ContinuousFunctions (S,T)) st S = TopSpaceMetr M & T is complete & G = H holds
( (MetricSpace_of_ContinuousFunctions (S,T)) | H is totally_bounded iff ( G is equicontinuous & ( for x being Point of S
for Hx being non empty Subset of T st Hx = { (f . x) where f is Function of S,T : f in H } holds
T | (Cl Hx) is compact ) ) )