let x be R_eal; :: 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 reconsider a = x as Real by XXREAL_0:14;
1. / x = 1 / a by A1, EXTREAL1:32, MESFUNC1:def 8;
then x * (1. / x) = a * (1 / a) by EXTREAL1:13
.= 1 by A1, XCMPLX_1:107 ;
hence ( x * (1. / x) = 1. & (1. / x) * x = 1. ) by MESFUNC1:def 8; :: thesis: verum