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

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

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

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

end;

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

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

end;

end;