theorem :: CLVECT_2:77
for X being ComplexUnitarySpace
for z being Complex
for seq being sequence of X st seq is bounded holds
z * seq is bounded