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 Z: S2 is convergent ; :: thesis: S2 is Cauchy
reconsider S2 = S2 as sequence of N ;
consider g being Element of N such that
A3: for r being Real st 0 < r holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
dist (S2 . m),g < r by Z, Def3;
let r be Real; :: according to TBSP_1:def 5 :: thesis: ( r > 0 implies ex p being Element of NAT st
for n, m being Element of NAT st p <= n & p <= m holds
dist (S2 . n),(S2 . m) < r )
assume 0 < r ; :: thesis: ex p being Element of NAT st
for n, m being Element of NAT st p <= n & p <= m holds
dist (S2 . n),(S2 . m) < r
then consider n being Element of NAT such that
A4: for m being Element of NAT st n <= m holds
dist (S2 . m),g < r / 2 by A3, XREAL_1:217;
take n ; :: thesis: for n, m being Element of NAT st n <= n & n <= m holds
dist (S2 . n),(S2 . m) < r
let m, m9 be Element of NAT ; :: thesis: ( n <= m & n <= m9 implies dist (S2 . m),(S2 . m9) < r )
assume that
A5: m >= n and
A6: m9 >= n ; :: thesis: dist (S2 . m),(S2 . m9) < r
A7: dist (S2 . m9),g < r / 2 by A4, A6;
dist (S2 . m),g < r / 2 by A4, A5;
then A8: (dist (S2 . m),g) + (dist g,(S2 . m9)) < (r / 2) + (r / 2) by A7, XREAL_1:10;
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 A8, XXREAL_0:2; :: thesis: verum