let seq1, seq2 be sequence of X; :: thesis: ( ( 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 ; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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; :: thesis: for n being Nat st n >= m holds
dist ((seq2 . n),(seq1 . n)) < r
let n be Nat; :: thesis: ( n >= m implies dist ((seq2 . n),(seq1 . n)) < r )
assume n >= m ; :: thesis: dist ((seq2 . n),(seq1 . n)) < r
hence dist ((seq2 . n),(seq1 . n)) < r by A3; :: thesis: verum