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:2, 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 1;
then |.x.| * |.(1. / x).| = a * (1 / a) by EXTREAL1:1;
hence |.x.| * |.(1. / x).| = 1. by A2, MESFUNC1:def 8, XCMPLX_1:106; :: thesis: verum

end;

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

then A5: |.x.| = - x by EXTREAL1:def 1
.= - a by SUPINF_2:2 ;
|.(1. / x).| = - (1. / x) by A3, A4, EXTREAL1:4, XREAL_1:142
.= - (1 / a) by A3, SUPINF_2:2 ;
then |.x.| * |.(1. / x).| = (- a) * (- (1 / a)) by A5, EXTREAL1:1
.= a * (1 / a) ;
hence |.x.| * |.(1. / x).| = 1. by A4, MESFUNC1:def 8, XCMPLX_1:106; :: thesis: verum

end;

end;