let M be non empty MetrSpace; :: thesis: 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 )
let A be non empty Subset of M; :: thesis: for S being sequence of (M | A)
for S9 being sequence of M st S = S9 holds
( S9 is Cauchy iff S is Cauchy )
let S be sequence of (M | A); :: thesis: for S9 being sequence of M st S = S9 holds
( S9 is Cauchy iff S is Cauchy )
let S9 be sequence of M; :: thesis: ( S = S9 implies ( S9 is Cauchy iff S is Cauchy ) )
assume A1: S = S9 ; :: thesis: ( S9 is Cauchy iff S is Cauchy )
thus ( S9 is Cauchy implies S is Cauchy ) :: thesis: ( S is Cauchy implies S9 is Cauchy )

proof

assume A2: S9 is Cauchy ; :: thesis: S is Cauchy
let r be Real; :: according to TBSP_1:def 4 :: thesis: ( r <= 0 or ex b₁ being set st
for b₂, b₃ being set holds
( not b₁ <= b₂ or not b₁ <= b₃ or not r <= dist ((S . b₂),(S . b₃)) ) )
assume r > 0 ; :: thesis: ex b₁ being set st
for b₂, b₃ being set holds
( not b₁ <= b₂ or not b₁ <= b₃ or not r <= dist ((S . b₂),(S . b₃)) )
then consider p being Nat such that
A3: for n, m being Nat st p <= n & p <= m holds
dist ((S9 . n),(S9 . m)) < r by A2;
take p ; :: thesis: for b₁, b₂ being set holds
( not p <= b₁ or not p <= b₂ or not r <= dist ((S . b₁),(S . b₂)) )
let n, m be Nat; :: thesis: ( not p <= n or not p <= m or not r <= dist ((S . n),(S . m)) )
assume that
A4: p <= n and
A5: p <= m ; :: thesis: not r <= dist ((S . n),(S . m))
dist ((S . n),(S . m)) = dist ((S9 . n),(S9 . m)) by A1, TOPMETR:def 1;
hence not r <= dist ((S . n),(S . m)) by A3, A4, A5; :: thesis: verum

end;

assume A6: S is Cauchy ; :: thesis: S9 is Cauchy
let r be Real; :: according to TBSP_1:def 4 :: thesis: ( r <= 0 or ex b₁ being set st
for b₂, b₃ being set holds
( not b₁ <= b₂ or not b₁ <= b₃ or not r <= dist ((S9 . b₂),(S9 . b₃)) ) )
assume r > 0 ; :: thesis: ex b₁ being set st
for b₂, b₃ being set holds
( not b₁ <= b₂ or not b₁ <= b₃ or not r <= dist ((S9 . b₂),(S9 . b₃)) )
then consider p being Nat such that
A7: for n, m being Nat st p <= n & p <= m holds
dist ((S . n),(S . m)) < r by A6;
take p ; :: thesis: for b₁, b₂ being set holds
( not p <= b₁ or not p <= b₂ or not r <= dist ((S9 . b₁),(S9 . b₂)) )
let n, m be Nat; :: thesis: ( not p <= n or not p <= m or not r <= dist ((S9 . n),(S9 . m)) )
assume that
A8: p <= n and
A9: p <= m ; :: thesis: not r <= dist ((S9 . n),(S9 . m))
dist ((S . n),(S . m)) = dist ((S9 . n),(S9 . m)) by A1, TOPMETR:def 1;
hence not r <= dist ((S9 . n),(S9 . m)) by A7, A8, A9; :: thesis: verum