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 )

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

( 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 A4:
for r being Real st r > 0 holds
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;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

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 )
;

end;