theorem Th27: :: COMPLEX2:29

for x, y being Complex holds x .|. y = (((Re x) * (Re y)) + ((Im x) * (Im y))) + (((- ((Re x) * (Im y))) + ((Im x) * (Re y))) * <i>)