let x be R_eal; :: thesis: ( x <> +infty & x <> -infty & x <> 0 implies ex y being R_eal st x * y = 1. )
assume A1: ( x <> +infty & x <> -infty & x <> 0 ) ; :: thesis: ex y being R_eal st x * y = 1.
then reconsider a = x as Real by XXREAL_0:14;
set b = 1 / a;
reconsider b = 1 / a as Real ;
A3: R_EAL b = b by MEASURE6:def 1;
take R_EAL b ; :: thesis: x * (R_EAL b) = 1.
a * b = 1 by A1, XCMPLX_1:88;
hence x * (R_EAL b) = 1. by A3, EXTREAL1:13, MESFUNC1:def 8; :: thesis: verum