for a being Element of F_Complex st 0 <= Re a & Im a = 0 holds
|.a.| = Re a