for c being Complex
for seq being Complex_Sequence st seq is bounded holds
c (#) seq is bounded by Lm4;