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:38; :: thesis: verum