for X being ComplexUnitarySpace
for seq being sequence of X
for k being Nat st seq is bounded holds
seq ^\ k is bounded by Th82;