theorem Th14: :: EXTREAL1:25

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