theorem :: COMPLEX2:39

for a, x, y being Complex holds (a * x) .|. y = x .|. ((a *') * y)