theorem :: RINFSUP1:26

for k being Nat
for seq being Real_Sequence st seq is bounded_above holds
seq ^\ k is bounded_above by SEQM_3:27;