:: deftheorem defines is_compared_to BHSP_3:def 2 :
for X being RealUnitarySpace
for seq1, seq2 being sequence of X holds
( seq1 is_compared_to seq2 iff 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 );