theorem Th36: :: COMPLEX2:38

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