theorem :: SIN_COS3:53

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