for M being non empty MetrSpace
for A being non empty Subset of M
for S being sequence of (M | A)
for S9 being sequence of M st S = S9 holds
( S9 is Cauchy iff S is Cauchy )