theorem :: FINSEQ_9:39

for a, b being Complex holds <*a*> /" <*b*> = <*(a * (b "))*>