let z1, z2 be Complex; :: thesis: z1 - z2 = ((Re z1) - (Re z2)) + (((Im z1) - (Im z2)) * <i>)
A1: z1 = (Re z1) + ((Im z1) * <i>) by Th13;
z1 - z2 = z1 + (- z2)
.= z1 + ((- (Re z2)) + ((- (Im z2)) * <i>)) by Lm22
.= ((Re z1) - (Re z2)) + (((Im z1) - (Im z2)) * <i>) by A1 ;
hence z1 - z2 = ((Re z1) - (Re z2)) + (((Im z1) - (Im z2)) * <i>) ; :: thesis: verum