theorem :: CLVECT_2:69

for X being ComplexUnitarySpace
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
||.((seq1 . n) - (seq2 . n)).|| < r )