theorem Th12: :: COMPLEX1:12

for a, b being Real holds
( Re (a + (b * <i>)) = a & Im (a + (b * <i>)) = b )