theorem :: XXREAL_3:87

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