let z be complex number ; :: thesis: ( Im z = 0 implies z *' = z )
( Re (z *' ) = Re z & Im (z *' ) = - (Im z) ) by Th112;
hence ( Im z = 0 implies z *' = z ) by Th9; :: thesis: verum