for M being non empty MetrSpace
for S being non empty compact TopSpace
for T being NormedLinearTopSpace
for U being compact Subset of T
for F being non empty Subset of (R_NormSpace_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
( ( Cl F is compact implies ( G is equibounded & G is equicontinuous ) ) & ( G is equicontinuous implies Cl F is compact ) )