theorem Th7: :: ASCOLI:7

for Z being RealNormSpace
for H being non empty Subset of (MetricSpaceNorm Z) st Z is complete holds
(MetricSpaceNorm Z) | (Cl H) is complete