for Rseq being Real_Sequence
for X being RealUnitarySpace
for seq being sequence of X st Rseq is bounded & seq is bounded holds
Rseq * seq is bounded