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