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 5 :: thesis: ( r <= 0 or ex b₁ being Element of NAT st
for b₂, b₃ being Element of NAT holds
( not b₁ <= b₂ or not b₁ <= b₃ or not r <= dist (S . b₂),(S . b₃) ) )
assume r > 0 ; :: thesis: ex b₁ being Element of NAT st
for b₂, b₃ being Element of NAT holds
( not b₁ <= b₂ or not b₁ <= b₃ or not r <= dist (S . b₂),(S . b₃) )
then consider p being Element of NAT such that
A3: for n, m being Element of NAT st p <= n & p <= m holds
dist (S9 . n),(S9 . m) < r by A2, TBSP_1:def 5;
take p ; :: thesis: for b₁, b₂ being Element of NAT holds
( not p <= b₁ or not p <= b₂ or not r <= dist (S . b₁),(S . b₂) )
let n, m be Element of 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 5 :: thesis: ( r <= 0 or ex b₁ being Element of NAT st
for b₂, b₃ being Element of NAT holds
( not b₁ <= b₂ or not b₁ <= b₃ or not r <= dist (S9 . b₂),(S9 . b₃) ) )
assume r > 0 ; :: thesis: ex b₁ being Element of NAT st
for b₂, b₃ being Element of NAT holds
( not b₁ <= b₂ or not b₁ <= b₃ or not r <= dist (S9 . b₂),(S9 . b₃) )
then consider p being Element of NAT such that
A7: for n, m being Element of NAT st p <= n & p <= m holds
dist (S . n),(S . m) < r by A6, TBSP_1:def 5;
take p ; :: thesis: for b₁, b₂ being Element of NAT holds
( not p <= b₁ or not p <= b₂ or not r <= dist (S9 . b₁),(S9 . b₂) )
let n, m be Element of 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