theorem Th21: :: CFDIFF_1:21

for k being Nat
for seq, seq1 being Complex_Sequence holds (seq (#) seq1) ^\ k = (seq ^\ k) (#) (seq1 ^\ k)