for X being ComplexUnitarySpace
for seq being sequence of X
for Cseq being Complex_Sequence st Cseq is bounded & seq is bounded holds
Cseq * seq is bounded