for n, k being Element of NAT
for x being Real st n <> 0 holds
((cos ((x + ((2 * PI) * k)) / n)) + ((sin ((x + ((2 * PI) * k)) / n)) * <i>)) |^ n = (cos x) + ((sin x) * <i>)