let x be Real; :: thesis: ( x <> 0 implies |.x.| * |.(1 / x).| = 1 )
assume x <> 0 ; :: thesis: |.x.| * |.(1 / x).| = 1
then ( |.x.| * |.(1 / x).| = |.(x * (1 / x)).| & |.(x * (1 / x)).| = |.1.| ) by COMPLEX1:65, XCMPLX_1:106;
hence |.x.| * |.(1 / x).| = 1 ; :: thesis: verum