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