let x be ext-real number ; :: thesis: ( x <> +infty & x <> -infty & x <> 0 implies ( x * (1 / x) = 1 & (1 / x) * x = 1 ) )
assume A1: ( x <> +infty & x <> -infty & x <> 0 ) ; :: thesis: ( x * (1 / x) = 1 & (1 / x) * x = 1 )
then x in REAL by XXREAL_0:14;
then reconsider a = x as real number ;
x * (1 / x) = a * (1 / a)
.= 1 by A1, XCMPLX_1:107 ;
hence ( x * (1 / x) = 1 & (1 / x) * x = 1 ) ; :: thesis: verum