let n be Element of NAT ; :: thesis: for z being Element of COMPLEX holds exp ((<i> * n) * z) = ((cos_C /. z) + (<i> * (sin_C /. z))) |^ n
let z be Element of COMPLEX ; :: thesis: exp ((<i> * n) * z) = ((cos_C /. z) + (<i> * (sin_C /. z))) |^ n
exp ((<i> * n) * z) = exp (<i> * (n * z))
.= (cos_C /. (n * z)) + (<i> * (sin_C /. (n * z))) by Th36 ;
hence exp ((<i> * n) * z) = ((cos_C /. z) + (<i> * (sin_C /. z))) |^ n by Th50; :: thesis: verum