theorem Th39: :: EUCLID_3:39

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