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