theorem :: SIN_COS3:26
for z being Complex holds exp (- z) = (cosh_C /. z) - (sinh_C /. z)