for r being Complex
for s being Complex_Sequence holds (r (#) s) *' = (r *') (#) (s *')