for seq being Complex_Sequence
for k being Nat holds
( (Re seq) ^\ k = Re (seq ^\ k) & (Im seq) ^\ k = Im (seq ^\ k) )