theorem :: COMPLEX1:81

for z1, z2 being Complex holds z1 + z2 = ((Re z1) + (Re z2)) + (((Im z1) + (Im z2)) * <i>)