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