let z be Complex; :: thesis: ( Re z = 0 implies z *' = - z )
assume A1: Re z = 0 ; :: thesis: z *' = - z
hence z *' = (- 0) + ((- (Im z)) * <i>)
.= - z by A1, Lm22 ;
:: thesis: verum