for z being Complex holds (Re z) + ((Im z) * <i>) = z