theorem Th15: :: ASCOLI2:15

for M being non empty MetrSpace
for S being non empty compact TopSpace
for T being non empty MetrSpace st S = TopSpaceMetr M holds
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 G = H & (MetricSpace_of_ContinuousFunctions (S,T)) | H is totally_bounded holds
G is equicontinuous