let a, b, x, y be Complex; :: thesis: <*a,b*> (#) <*x,y*> = <*(a * x),(b * y)*>
<*a,b*> (#) <*x,y*> = (<*a*> (#) <*x*>) ^ <*(b * y)*> by FMA;
hence <*a,b*> (#) <*x,y*> = <*(a * x),(b * y)*> by AMB; :: thesis: verum