theorem :: COMPLFLD:72

for z being Element of F_Complex st z <> 0. F_Complex holds
|.(z ").| = |.z.| "