let M be non empty MetrSpace; :: thesis: for A being non empty Subset of M
for S being sequence of (M | A) holds S is sequence of M
let A be non empty Subset of M; :: thesis: for S being sequence of (M | A) holds S is sequence of M
let S be sequence of (M | A); :: thesis: S is sequence of M
A c= the carrier of M ;
then the carrier of (M | A) c= the carrier of M by TOPMETR:def 2;
hence S is sequence of M by FUNCT_2:7; :: thesis: verum