theorem :: EXTREAL1:27

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