let x be Real; :: thesis: exp_R (- x) = 1 / (exp_R x)
reconsider x = x as Real ;
(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