let z be Element of F_Complex; :: thesis: |.(- z).| = |.z.|
reconsider z1 = z as Element of COMPLEX by Def1;
- z1 = - z by Th2;
hence |.(- z).| = |.z.| by COMPLEX1:52; :: thesis: verum