theorem Th23: :: COMPLSP2:27

for z being Complex holds z - (z *') = (2 * (Im z)) * <i>