theorem :: CFCONT_1:15

for g being Complex
for seq being Complex_Sequence
for h being PartFunc of COMPLEX,COMPLEX st h is total holds
(g (#) h) /* seq = g (#) (h /* seq)