for seq being Complex_Sequence
for Nseq being increasing sequence of NAT holds
( Re (seq * Nseq) = (Re seq) * Nseq & Im (seq * Nseq) = (Im seq) * Nseq )