for seq being Complex_Sequence
for Nseq being V42() sequence of NAT
for n being Nat holds (seq * Nseq) . n = seq . (Nseq . n)