for k being Nat
for seq being Real_Sequence st seq is bounded holds
seq ^\ k is bounded by SEQM_3:29;