let a, x, y be Complex; :: thesis: x .|. (a * y) = (a *') * (x .|. y)
thus x .|. (a * y) = x * ((a *') * (y *')) by COMPLEX1:35
.= (a *') * (x .|. y) ; :: thesis: verum