let M be MetrStruct ; :: thesis: for S being sequence of M holds S is sequence of (TopSpaceMetr M)
let S be sequence of M; :: thesis: S is sequence of (TopSpaceMetr M)
the carrier of M = the carrier of (TopSpaceMetr M) by TOPMETR:12;
hence S is sequence of (TopSpaceMetr M) ; :: thesis: verum