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