for x, y being Element of COMPLEX holds Im (x .|. y) = (- ((Re x) * (Im y))) + ((Im x) * (Re y))