let x be R_eal; :: thesis: ( -infty < x & x < +infty & x <> 0 implies |.x.| * |.(1. / x).| = 1. )
assume that
A1: ( -infty < x & x < +infty ) and
A2: x <> 0 ; :: thesis: |.x.| * |.(1. / x).| = 1.
reconsider a = x as Real by A1, XXREAL_0:14;
A3: 1. / x = 1 / a by EXTREAL1:32, MESFUNC1:def 8;

per cases ( 0 <= x or not 0 <= x ) ;

suppose 0 <= x ; :: thesis: |.x.| * |.(1. / x).| = 1.

then ( |.x.| = a & |.(1. / x).| = 1 / a ) by A3, EXTREAL1:def 3;
then |.x.| * |.(1. / x).| = a * (1 / a) by EXTREAL1:13;
hence |.x.| * |.(1. / x).| = 1. by A2, MESFUNC1:def 8, XCMPLX_1:107; :: thesis: verum

end;

suppose A4: not 0 <= x ; :: thesis: |.x.| * |.(1. / x).| = 1.

then A5: |.x.| = - x by EXTREAL1:def 3
.= - a by SUPINF_2:3 ;
|.(1. / x).| = - (1. / x) by A3, A4, EXTREAL1:37, XREAL_1:144
.= - (1 / a) by A3, SUPINF_2:3 ;
then |.x.| * |.(1. / x).| = (- a) * (- (1 / a)) by A5, EXTREAL1:13
.= a * (1 / a) ;
hence |.x.| * |.(1. / x).| = 1. by A4, MESFUNC1:def 8, XCMPLX_1:107; :: thesis: verum

end;

end;