for X being ComplexUnitarySpace
for seq1, seq2 being sequence of X st ex k being Nat st
for n being Nat st n >= k holds
seq1 . n = seq2 . n holds
seq1 is_compared_to seq2