let x be ExtReal; :: thesis: ( ( x = +infty or x = -infty ) implies |.x.| * |.(1. / x).| = 0 )
assume ( x = +infty or x = -infty ) ; :: thesis: |.x.| * |.(1. / x).| = 0
then |.(1. / x).| = 0 by Def1;
hence |.x.| * |.(1. / x).| = 0 ; :: thesis: verum