let z be complex number ; :: thesis: z - (z *') = (2 * (Im z)) * <i>
z is Element of COMPLEX by XCMPLX_0:def 2;
then z - (z *') = ((Re z) - (Re (z *'))) + (((Im z) - (Im (z *'))) * <i>) by COMPLEX1:def 12
.= ((Re z) - (Re (z *'))) + (((Im z) - (- (Im z))) * <i>) by COMPLEX1:112
.= ((Re z) - (Re z)) + (((Im z) - (- (Im z))) * <i>) by COMPLEX1:112
.= (2 * (Im z)) * <i> ;
hence z - (z *') = (2 * (Im z)) * <i> ; :: thesis: verum