let z be Complex; :: thesis: ( Re (z + (z *')) = 2 * (Re z) & Im (z + (z *')) = 0 )
thus Re (z + (z *')) = (Re z) + (Re (z *')) by Th8
.= (Re z) + (Re z) by Th27
.= 2 * (Re z) ; :: thesis: Im (z + (z *')) = 0
thus Im (z + (z *')) = (Im z) + (Im (z *')) by Th8
.= (Im z) + (- (Im z)) by Th27
.= 0 ; :: thesis: verum