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