theorem :: EXTREAL1:26

for x being ExtReal st ( x = +infty or x = -infty ) holds
|.x.| * |.(1. / x).| = 0