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:112
.= 2 * (Re z) ; :: thesis: verum