let N be non empty MetrStruct ; :: thesis: for S2 being sequence of N st N is symmetric holds
( S2 is Cauchy iff for r being Real st r > 0 holds
ex p being Element of NAT st
for n, k being Element of NAT st p <= n holds
dist (S2 . (n + k)),(S2 . n) < r )
let S2 be sequence of N; :: thesis: ( N is symmetric implies ( S2 is Cauchy iff for r being Real st r > 0 holds
ex p being Element of NAT st
for n, k being Element of NAT st p <= n holds
dist (S2 . (n + k)),(S2 . n) < r ) )
assume A1: N is symmetric ; :: thesis: ( S2 is Cauchy iff for r being Real st r > 0 holds
ex p being Element of NAT st
for n, k being Element of NAT st p <= n holds
dist (S2 . (n + k)),(S2 . n) < r )
thus ( S2 is Cauchy implies for r being Real st r > 0 holds
ex p being Element of NAT st
for n, k being Element of NAT st p <= n holds
dist (S2 . (n + k)),(S2 . n) < r ) :: thesis: ( ( for r being Real st r > 0 holds
ex p being Element of NAT st
for n, k being Element of NAT st p <= n holds
dist (S2 . (n + k)),(S2 . n) < r ) implies S2 is Cauchy )

proof

assume A2: S2 is Cauchy ; :: thesis: for r being Real st r > 0 holds
ex p being Element of NAT st
for n, k being Element of NAT st p <= n holds
dist (S2 . (n + k)),(S2 . n) < r
let r be Real; :: thesis: ( r > 0 implies ex p being Element of NAT st
for n, k being Element of NAT st p <= n holds
dist (S2 . (n + k)),(S2 . n) < r )
assume 0 < r ; :: thesis: ex p being Element of NAT st
for n, k being Element of NAT st p <= n holds
dist (S2 . (n + k)),(S2 . n) < r
then consider p being Element of NAT such that
A3: for n, m being Element of NAT st p <= n & p <= m holds
dist (S2 . n),(S2 . m) < r by A2, Def5;
take p ; :: thesis: for n, k being Element of NAT st p <= n holds
dist (S2 . (n + k)),(S2 . n) < r
let n, k be Element of NAT ; :: thesis: ( p <= n implies dist (S2 . (n + k)),(S2 . n) < r )
assume A4: p <= n ; :: thesis: dist (S2 . (n + k)),(S2 . n) < r
n <= n + k by NAT_1:11;
then ( p <= n + k & p <= n ) by A4, XXREAL_0:2;
hence dist (S2 . (n + k)),(S2 . n) < r by A3; :: thesis: verum

end;

assume A5: for r being Real st r > 0 holds
ex p being Element of NAT st
for n, k being Element of NAT st p <= n holds
dist (S2 . (n + k)),(S2 . n) < r ; :: thesis: S2 is Cauchy
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 p being Element of NAT such that
A6: for n, k being Element of NAT st p <= n holds
dist (S2 . (n + k)),(S2 . n) < r by A5;
take p ; :: thesis: for n, m being Element of NAT st p <= n & p <= m holds
dist (S2 . n),(S2 . m) < r
let n, m be Element of NAT ; :: thesis: ( p <= n & p <= m implies dist (S2 . n),(S2 . m) < r )
assume A7: ( p <= n & p <= m ) ; :: thesis: dist (S2 . n),(S2 . m) < r

per cases ( n <= m or m <= n ) ;

suppose n <= m ; :: thesis: dist (S2 . n),(S2 . m) < r

then consider k being Nat such that
A8: m = n + k by NAT_1:10;
reconsider m' = m, n' = n, k = k as Element of NAT by ORDINAL1:def 13;
m = n + k by A8;
then dist (S2 . m'),(S2 . n') < r by A6, A7;
hence dist (S2 . n),(S2 . m) < r by A1, METRIC_1:3; :: thesis: verum

end;

suppose m <= n ; :: thesis: dist (S2 . n),(S2 . m) < r

then consider k being Nat such that
A9: n = m + k by NAT_1:10;
reconsider k = k as Element of NAT by ORDINAL1:def 13;
n = m + k by A9;
hence dist (S2 . n),(S2 . m) < r by A6, A7; :: thesis: verum

end;

end;