for M being MetrStruct
for S being sequence of M holds S is sequence of (TopSpaceMetr M)