let z be Element of COMPLEX ; :: thesis: (exp z) * (exp (- z)) = 1
thus (exp z) * (exp (- z)) = exp (z + (- z)) by SIN_COS:24
.= 1 by SIN_COS:54, SIN_COS:56 ; :: thesis: verum