let z be Complex; :: 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 Th12; :: thesis: verum