let N be non empty symmetric MetrStruct ; :: thesis: for S2 being sequence of N holds
( S2 is Cauchy iff for r being Real st r > 0 holds
ex p being Nat st
for n, k being Nat st p <= n holds
dist ((S2 . (n + k)),(S2 . n)) < r )
let S2 be sequence of N; :: thesis: ( S2 is Cauchy iff for r being Real st r > 0 holds
ex p being Nat st
for n, k being 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 Nat st
for n, k being Nat st p <= n holds
dist ((S2 . (n + k)),(S2 . n)) < r ) :: thesis: ( ( for r being Real st r > 0 holds
ex p being Nat st
for n, k being Nat st p <= n holds
dist ((S2 . (n + k)),(S2 . n)) < r ) implies S2 is Cauchy )

proof

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

end;

assume A4: for r being Real st r > 0 holds
ex p being Nat st
for n, k being 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 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 p being Nat such that
A5: for n, k being Nat st p <= n holds
dist ((S2 . (n + k)),(S2 . n)) < r by A4;
take p ; :: thesis: for n, m being Nat st p <= n & p <= m holds
dist ((S2 . n),(S2 . m)) < r
let n, m be Nat; :: thesis: ( p <= n & p <= m implies dist ((S2 . n),(S2 . m)) < r )
assume that
A6: p <= n and
A7: 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 m9 = m, n9 = n, k = k as Nat ;
m = n + k by A8;
then dist ((S2 . m9),(S2 . n9)) < r by A5, A6;
hence dist ((S2 . n),(S2 . m)) < r ; :: 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 Nat ;
n = m + k by A9;
hence dist ((S2 . n),(S2 . m)) < r by A5, A7; :: thesis: verum

end;

end;