theorem :: RINFSUP1:27

for k being Nat
for seq being Real_Sequence st seq is V96() holds
seq ^\ k is V96() by SEQM_3:28;