let x be real number ; :: thesis: exp_R (- x) = 1 / (exp_R x)
reconsider x = x as Real by XREAL_0:def 1;
(exp_R (- x)) * (exp_R x) = exp_R ((- x) + x) by SIN_COS:50
.= 1 by SIN_COS:51 ;
hence exp_R (- x) = 1 / (exp_R x) by XCMPLX_1:73; :: thesis: verum