theorem :: COMPLEX1:41

for z being Complex holds
( Re (z + (z *')) = 2 * (Re z) & Im (z + (z *')) = 0 )