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