for S being non empty compact TopSpace
for T being NormedLinearTopSpace st T is complete holds
for F being non empty Subset of (R_NormSpace_of_ContinuousFunctions (S,T))
for H being non empty Subset of (MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) st H = F holds
( Cl F is compact iff (MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) | H is totally_bounded )