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 Th48
.= (Re z) - (Re z) by Th112
.= 0 ; :: thesis: Im (z - (z *')) = 2 * (Im z)
thus Im (z - (z *')) = (Im z) - (Im (z *')) by Th48
.= (Im z) - (- (Im z)) by Th112
.= 2 * (Im z) ; :: thesis: verum