for N being non empty symmetric MetrStruct
for S2 being sequence of N holds
( S2 is Cauchy iff for r being Real st r > 0 holds
ex p being Nat st
for n, k being Nat st p <= n holds
dist ((S2 . (n + k)),(S2 . n)) < r )