theorem :: CFCONT_1:16

for X being set
for seq being Complex_Sequence
for h being PartFunc of COMPLEX,COMPLEX st rng seq c= dom (h | X) & h " {0} = {} holds
((h ^) | X) /* seq = ((h | X) /* seq) "