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