theorem :: CFCONT_1:12

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
Re ((h /* seq) * Ns) = Re (h /* (seq * Ns))