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:55
.= 1 by SIN_COS:56 ;
hence exp_R (- x) = 1 / (exp_R x) by XCMPLX_1:74; :: thesis: verum