let z be Complex; :: thesis: z + (z *') = 2 * (Re z)
z + (z *') = ((Re z) + (Re (z *'))) + (((Im z) + (Im (z *'))) * <i>) by COMPLEX1:81
.= ((Re z) + (Re (z *'))) + (((Im z) + (- (Im z))) * <i>) by COMPLEX1:27
.= (Re z) + (Re z) by COMPLEX1:27
.= 2 * (Re z) ;
hence z + (z *') = 2 * (Re z) ; :: thesis: verum