let x be ExtReal; :: thesis: ( x <> +infty & x <> -infty & x <> 0 implies ( x * (1 / x) = 1 & (1 / x) * x = 1 ) )
assume that
A1: ( x <> +infty & x <> -infty ) and
A2: x <> 0 ; :: thesis: ( x * (1 / x) = 1 & (1 / x) * x = 1 )
x in REAL by A1, XXREAL_0:14;
then reconsider a = x as Real ;
x * (1 / x) = a * (1 / a)
.= 1 by A2, XCMPLX_1:106 ;
hence ( x * (1 / x) = 1 & (1 / x) * x = 1 ) ; :: thesis: verum