let z be complex number ; :: thesis: ( Re (z *') = Re z & Im (z *') = - (Im z) )
z *' = (Re z) + ((- (Im z)) * <i>) ;
hence ( Re (z *') = Re z & Im (z *') = - (Im z) ) by Th28; :: thesis: verum