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