let z be Element of F_Complex; :: thesis: (Re z) + (Re (z *')) = 2 * (Re z)
thus (Re z) + (Re (z *')) = (Re z) + (Re z) by COMPLEX1:27
.= 2 * (Re z) ; :: thesis: verum