let z be complex number ; :: thesis: z + (z *') = 2 * (Re z)
z is Element of COMPLEX by XCMPLX_0:def 2;
then z + (z *') = ((Re z) + (Re (z *'))) + (((Im z) + (Im (z *'))) * <i>) by COMPLEX1:def 9
.= ((Re z) + (Re (z *'))) + (((Im z) + (- (Im z))) * <i>) by COMPLEX1:112
.= (Re z) + (Re z) by COMPLEX1:112
.= 2 * (Re z) ;
hence z + (z *') = 2 * (Re z) ; :: thesis: verum