theorem :: CFCONT_1:13

for seq being Complex_Sequence
for h being PartFunc of COMPLEX,COMPLEX
for Ns being V42() sequence of NAT st rng seq c= dom h holds
Im ((h /* seq) * Ns) = Im (h /* (seq * Ns))