let x be ExtReal; :: thesis: ( x <> 0 implies |.(1. / x).| = 1. / |.x.| )
assume A1: x <> 0 ; :: thesis: |.(1. / x).| = 1. / |.x.|

per cases ( x = +infty or x = -infty or ( x <> +infty & x <> -infty ) ) ;

suppose A2: x = +infty ; :: thesis: |.(1. / x).| = 1. / |.x.|

then |.(1. / x).| = 0 by Def1;
hence |.(1. / x).| = 1. / |.x.| by A2, Def1; :: thesis: verum

end;

suppose x = -infty ; :: thesis: |.(1. / x).| = 1. / |.x.|

then ( |.(1. / x).| = 0 & |.x.| = +infty ) by Def1, XXREAL_3:5;
hence |.(1. / x).| = 1. / |.x.| ; :: thesis: verum

end;

suppose A3: ( x <> +infty & x <> -infty ) ; :: thesis: |.(1. / x).| = 1. / |.x.|

A4: 0 < |.x.| by A1, Th4;
A5: x < +infty by A3, XXREAL_0:4;
-infty <= x by XXREAL_0:5;
then A6: -infty < x by A3, XXREAL_0:1;
then - +infty < x by XXREAL_3:def 3;
then A7: |.x.| < +infty by A5, Th11;
|.(1. / x).| * |.x.| = 1. by A1, A6, A5, Th14;
hence |.(1. / x).| = 1. / |.x.| by A4, A7, XXREAL_3:88; :: thesis: verum

end;

end;