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