for z being Complex holds z + (z *') = 2 * (Re z)