let z be Complex; :: thesis: exp (- z) = (cosh_C /. z) - (sinh_C /. z)
(cosh_C /. z) - (sinh_C /. z) = (((exp z) + (exp (- z))) / 2) - (sinh_C /. z) by Def4
.= (((exp z) + (exp (- z))) / 2) - (((exp z) - (exp (- z))) / 2) by Def3
.= ((exp (- z)) + (exp (- z))) / 2
.= (((Re (exp (- z))) + (Re (exp (- z)))) + (((Im (exp (- z))) + (Im (exp (- z)))) * <i>)) / 2 by COMPLEX1:81
.= ((2 * (Re (exp (- z)))) + ((2 * (Im (exp (- z)))) * <i>)) / 2
.= ((Re (2 * (exp (- z)))) + ((2 * (Im (exp (- z)))) * <i>)) / 2 by COMSEQ_3:17
.= ((Re (2 * (exp (- z)))) + ((Im (2 * (exp (- z)))) * <i>)) / 2 by COMSEQ_3:17
.= (2 * (exp (- z))) / 2 by COMPLEX1:13
.= (exp (- z)) * 1 ;
hence exp (- z) = (cosh_C /. z) - (sinh_C /. z) ; :: thesis: verum