let z be Complex; :: thesis: exp (<i> * z) = (cos_C /. z) + (<i> * (sin_C /. z))
reconsider z = z as Element of COMPLEX by XCMPLX_0:def 2;
(cos_C /. z) + (<i> * (sin_C /. z)) = (((exp (<i> * z)) + (exp (- (<i> * z)))) / 2) + (<i> * (sin_C /. z)) by Def2
.= (((exp (<i> * z)) + (exp (- (<i> * z)))) / 2) + (<i> * (((exp (<i> * z)) - (exp (- (<i> * z)))) / (2 * <i>))) by Def1
.= ((exp (<i> * z)) + (((exp (- (<i> * z))) + (exp (<i> * z))) - (exp (- (<i> * z))))) / 2
.= (((Re (exp (<i> * z))) + (Re (exp (<i> * z)))) + (((Im (exp (<i> * z))) + (Im (exp (<i> * z)))) * <i>)) / 2 by COMPLEX1:81
.= ((2 * (Re (exp (<i> * z)))) + ((2 * (Im (exp (<i> * z)))) * <i>)) / 2
.= ((Re (2 * (exp (<i> * z)))) + ((2 * (Im (exp (<i> * z)))) * <i>)) / 2 by COMSEQ_3:17
.= ((Re (2 * (exp (<i> * z)))) + ((Im (2 * (exp (<i> * z)))) * <i>)) / 2 by COMSEQ_3:17
.= (2 * (exp (<i> * z))) / 2 by COMPLEX1:13 ;
hence exp (<i> * z) = (cos_C /. z) + (<i> * (sin_C /. z)) ; :: thesis: verum