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