theorem :: CFCONT_1:13
for seq being Complex_Sequence
for h being PartFunc of COMPLEX,COMPLEX
for Ns being increasing sequence of NAT st rng seq c= dom h holds
Im ((h /* seq) * Ns) = Im (h /* (seq * Ns))