theorem Th6: :: ASCOLI:6

for Z being RealNormSpace holds
( Z is complete iff MetricSpaceNorm Z is complete )