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