theorem :: COMPLEX1:84

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