theorem :: COMPLEX2:37

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