theorem AM3: :: FINSEQ_9:46

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