let z be Element of F_Complex ; :: thesis: ( Im z = 0 implies z *' = z )
A1: the carrier of F_Complex = COMPLEX by COMPLFLD:def 1;
assume Im z = 0 ; :: thesis: z *' = z
hence z *' = z by A1, COMPLEX1:124; :: thesis: verum