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