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