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