for g being Complex
for seq being Complex_Sequence
for h being PartFunc of COMPLEX,COMPLEX st rng seq c= dom h holds
(g (#) h) /* seq = g (#) (h /* seq)