for k being Nat
for seq being Real_Sequence holds (seq ") ^\ k = (seq ^\ k) "