let seq1, seq2 be sequence of X; ( ( for r being Real st r > 0 holds
ex m being Nat st
for n being Nat st n >= m holds
dist ((seq1 . n),(seq2 . n)) < r ) implies for r being Real st r > 0 holds
ex m being Nat st
for n being Nat st n >= m holds
dist ((seq2 . n),(seq1 . n)) < r )
assume A2:
for r being Real st r > 0 holds
ex m being Nat st
for n being Nat st n >= m holds
dist ((seq1 . n),(seq2 . n)) < r
; for r being Real st r > 0 holds
ex m being Nat st
for n being Nat st n >= m holds
dist ((seq2 . n),(seq1 . n)) < r
let r be Real; ( r > 0 implies ex m being Nat st
for n being Nat st n >= m holds
dist ((seq2 . n),(seq1 . n)) < r )
assume
r > 0
; ex m being Nat st
for n being Nat st n >= m holds
dist ((seq2 . n),(seq1 . n)) < r
then consider k being Nat such that
A3:
for n being Nat st n >= k holds
dist ((seq1 . n),(seq2 . n)) < r
by A2;
take m = k; for n being Nat st n >= m holds
dist ((seq2 . n),(seq1 . n)) < r
let n be Nat; ( n >= m implies dist ((seq2 . n),(seq1 . n)) < r )
assume
n >= m
; dist ((seq2 . n),(seq1 . n)) < r
hence
dist ((seq2 . n),(seq1 . n)) < r
by A3; verum