theorem :: COMSEQ_2:5

for s, s9 being Complex_Sequence holds (s (#) s9) *' = (s *') (#) (s9 *')