for seq being Complex_Sequence
for h being PartFunc of COMPLEX,COMPLEX st rng seq c= dom (h ^) holds
(h ^) /* seq = (h /* seq) "