theorem :: FINSEQ_9:47

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