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