let z be complex number ; :: thesis: ( Re (z - (z *')) = 0 & Im (z - (z *')) = 2 * (Im z) )
thus Re (z - (z *')) = (Re z) - (Re (z *')) by Th19
.= (Re z) - (Re z) by Th27
.= 0 ; :: thesis: Im (z - (z *')) = 2 * (Im z)
thus Im (z - (z *')) = (Im z) - (Im (z *')) by Th19
.= (Im z) - (- (Im z)) by Th27
.= 2 * (Im z) ; :: thesis: verum