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)) + (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