theorem :: FRECHET2:27

for M being non empty MetrStruct
for S being sequence of (TopSpaceMetr M) holds S is sequence of M by TOPMETR:12;