let N be non empty MetrStruct ; :: thesis: for S2 being sequence of N st N is triangle & N is symmetric & S2 is convergent holds

S2 is Cauchy

let S2 be sequence of N; :: thesis: ( N is triangle & N is symmetric & S2 is convergent implies S2 is Cauchy )

assume that

A1: N is triangle and

A2: N is symmetric ; :: thesis: ( not S2 is convergent or S2 is Cauchy )

reconsider N = N as non empty symmetric MetrStruct by A2;

assume A3: S2 is convergent ; :: thesis: S2 is Cauchy

reconsider S2 = S2 as sequence of N ;

consider g being Element of N such that

A4: for r being Real st 0 < r holds

ex n being Nat st

for m being Nat st n <= m holds

dist ((S2 . m),g) < r by A3;

let r be Real; :: according to TBSP_1:def 4 :: thesis: ( r > 0 implies ex p being Nat st

for n, m being Nat st p <= n & p <= m holds

dist ((S2 . n),(S2 . m)) < r )

assume 0 < r ; :: thesis: ex p being Nat st

for n, m being Nat st p <= n & p <= m holds

dist ((S2 . n),(S2 . m)) < r

then consider n being Nat such that

A5: for m being Nat st n <= m holds

dist ((S2 . m),g) < r / 2 by A4, XREAL_1:215;

take n ; :: thesis: for n, m being Nat st n <= n & n <= m holds

dist ((S2 . n),(S2 . m)) < r

let m, m9 be Nat; :: thesis: ( n <= m & n <= m9 implies dist ((S2 . m),(S2 . m9)) < r )

assume that

A6: m >= n and

A7: m9 >= n ; :: thesis: dist ((S2 . m),(S2 . m9)) < r

A8: dist ((S2 . m9),g) < r / 2 by A5, A7;

dist ((S2 . m),g) < r / 2 by A5, A6;

then A9: (dist ((S2 . m),g)) + (dist (g,(S2 . m9))) < (r / 2) + (r / 2) by A8, XREAL_1:8;

dist ((S2 . m),(S2 . m9)) <= (dist ((S2 . m),g)) + (dist (g,(S2 . m9))) by A1, METRIC_1:4;

hence dist ((S2 . m),(S2 . m9)) < r by A9, XXREAL_0:2; :: thesis: verum

S2 is Cauchy

let S2 be sequence of N; :: thesis: ( N is triangle & N is symmetric & S2 is convergent implies S2 is Cauchy )

assume that

A1: N is triangle and

A2: N is symmetric ; :: thesis: ( not S2 is convergent or S2 is Cauchy )

reconsider N = N as non empty symmetric MetrStruct by A2;

assume A3: S2 is convergent ; :: thesis: S2 is Cauchy

reconsider S2 = S2 as sequence of N ;

consider g being Element of N such that

A4: for r being Real st 0 < r holds

ex n being Nat st

for m being Nat st n <= m holds

dist ((S2 . m),g) < r by A3;

let r be Real; :: according to TBSP_1:def 4 :: thesis: ( r > 0 implies ex p being Nat st

for n, m being Nat st p <= n & p <= m holds

dist ((S2 . n),(S2 . m)) < r )

assume 0 < r ; :: thesis: ex p being Nat st

for n, m being Nat st p <= n & p <= m holds

dist ((S2 . n),(S2 . m)) < r

then consider n being Nat such that

A5: for m being Nat st n <= m holds

dist ((S2 . m),g) < r / 2 by A4, XREAL_1:215;

take n ; :: thesis: for n, m being Nat st n <= n & n <= m holds

dist ((S2 . n),(S2 . m)) < r

let m, m9 be Nat; :: thesis: ( n <= m & n <= m9 implies dist ((S2 . m),(S2 . m9)) < r )

assume that

A6: m >= n and

A7: m9 >= n ; :: thesis: dist ((S2 . m),(S2 . m9)) < r

A8: dist ((S2 . m9),g) < r / 2 by A5, A7;

dist ((S2 . m),g) < r / 2 by A5, A6;

then A9: (dist ((S2 . m),g)) + (dist (g,(S2 . m9))) < (r / 2) + (r / 2) by A8, XREAL_1:8;

dist ((S2 . m),(S2 . m9)) <= (dist ((S2 . m),g)) + (dist (g,(S2 . m9))) by A1, METRIC_1:4;

hence dist ((S2 . m),(S2 . m9)) < r by A9, XXREAL_0:2; :: thesis: verum