let z be Element of F_Complex ; :: thesis: ( Im z = 0 implies z *' = z )
assume Im z = 0 ; :: thesis: z *' = z
hence z *' = z by COMPLEX1:124; :: thesis: verum