theorem AM2: :: FINSEQ_9:45

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