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