theorem :: ABSVALUE:6

for x being Real st x <> 0 holds
|.x.| * |.(1 / x).| = 1