theorem Th40: :: EUCLID_3:40

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