for n being Element of NAT
for z being Element of COMPLEX holds exp ((<i> * n) * z) = ((cos_C /. z) + (<i> * (sin_C /. z))) |^ n