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 b1 being set st
for b2, b3 being set holds
( not b1 <= b2 or not b1 <= b3 or not r <= dist ((S . b2),(S . b3)) ) )
assume r > 0 ; :: thesis: ex b1 being set st
for b2, b3 being set holds
( not b1 <= b2 or not b1 <= b3 or not r <= dist ((S . b2),(S . b3)) )
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 b1, b2 being set holds
( not p <= b1 or not p <= b2 or not r <= dist ((S . b1),(S . b2)) )
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 b1 being set st
for b2, b3 being set holds
( not b1 <= b2 or not b1 <= b3 or not r <= dist ((S9 . b2),(S9 . b3)) ) )
assume r > 0 ; :: thesis: ex b1 being set st
for b2, b3 being set holds
( not b1 <= b2 or not b1 <= b3 or not r <= dist ((S9 . b2),(S9 . b3)) )
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 b1, b2 being set holds
( not p <= b1 or not p <= b2 or not r <= dist ((S9 . b1),(S9 . b2)) )
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