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