let x be ExtReal; :: 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 Element of REAL by A1, XXREAL_0:14;
A3: 1. / x = 1 / a by Th2;

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

end;

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

then A5: |.x.| = - x by Def1
.= - a by SUPINF_2:2 ;
1. / x < 0 by A3, A4;
then |.(1. / x).| = - (1. / x) by Def1
.= - (1 / a) by A3, SUPINF_2:2 ;
then |.x.| * |.(1. / x).| = (- a) * (- (1 / a)) by A5, XXREAL_3:def 5
.= a * (1 / a) ;
hence |.x.| * |.(1. / x).| = 1. by A4, XCMPLX_1:106; :: thesis: verum

end;

end;