theorem :: FRECHET2:26

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