theorem :: COMPLFLD:61

for z being Element of F_Complex holds |.(- z).| = |.z.|