for a being Element of F_Complex holds (Re a) + (Re (a *')) = 2 * (Re a)