:: deftheorem defines bounded CLVECT_2:def 10 :
for X being ComplexUnitarySpace
for seq being sequence of X holds
( seq is bounded iff ex M being Real st
( M > 0 & ( for n being Nat holds ||.(seq . n).|| <= M ) ) );