let z be Element of COMPLEX ; :: thesis: (exp z) * (exp (- z)) = 1
thus (exp z) * (exp (- z)) = exp (z + (- z)) by SIN_COS:23
.= 1 by SIN_COS:49, SIN_COS:51 ; :: thesis: verum