for Z being RealNormSpace
for F being non empty Subset of Z
for H being non empty Subset of (MetricSpaceNorm Z) st Z is complete & H = F & (MetricSpaceNorm Z) | H is totally_bounded holds
( Cl H is sequentially_compact & (MetricSpaceNorm Z) | (Cl H) is compact & Cl F is compact )