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 )
assume S2 is convergent ; :: thesis: S2 is Cauchy
then 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 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 0 < r / 2 by XREAL_1:217;
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;
take n ; :: thesis: for n, m being Element of NAT st n <= n & n <= m holds
dist (S2 . n),(S2 . m) < r
let m, m' be Element of NAT ; :: thesis: ( n <= m & n <= m' implies dist (S2 . m),(S2 . m') < r )
assume A5: ( m >= n & m' >= n ) ; :: thesis: dist (S2 . m),(S2 . m') < r
then A6: dist (S2 . m),g < r / 2 by A4;
dist (S2 . m'),g < r / 2 by A4, A5;
then dist g,(S2 . m') < r / 2 by A2, METRIC_1:3;
then A7: (dist (S2 . m),g) + (dist g,(S2 . m')) < (r / 2) + (r / 2) by A6, XREAL_1:10;
dist (S2 . m),(S2 . m') <= (dist (S2 . m),g) + (dist g,(S2 . m')) by A1, METRIC_1:4;
hence dist (S2 . m),(S2 . m') < r by A7, XXREAL_0:2; :: thesis: verum