theorem AMB: :: FINSEQ_9:38

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