theorem Th20: :: CFDIFF_1:20

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