let z be complex number ; :: thesis: ( Re z = 0 implies z *' = - z )
a1: z in COMPLEX by XCMPLX_0:def 2;
assume A1: Re z = 0 ; :: thesis: z *' = - z
hence z *' = (- 0) + ((- (Im z)) * <i>)
.= - z by a1, A1, Def11 ;
:: thesis: verum