for NrSp being RealNormSpace
for S being Subset of NrSp
for T being Subset of (MetricSpaceNorm NrSp) st S = T holds
( S is compact iff T is sequentially_compact )