theorem Th18: :: SEQM_3:18

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