theorem Th13: :: COMPLEX1:13

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