theorem :: CLVECT_2:81

for X being ComplexUnitarySpace
for seq1, seq2 being sequence of X st seq1 is bounded & seq1 is_compared_to seq2 holds
seq2 is bounded