let z be Complex; :: thesis: z - (z *') = (2 * (Im z)) * <i>
z - (z *') = ((Re z) - (Re (z *'))) + (((Im z) - (Im (z *'))) * <i>) by COMPLEX1:84
.= ((Re z) - (Re (z *'))) + (((Im z) - (- (Im z))) * <i>) by COMPLEX1:27
.= ((Re z) - (Re z)) + (((Im z) - (- (Im z))) * <i>) by COMPLEX1:27
.= (2 * (Im z)) * <i> ;
hence z - (z *') = (2 * (Im z)) * <i> ; :: thesis: verum