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