theorem :: COMSEQ_2:7

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