theorem :: SIN_COS3:30
for n being Element of NAT holds exp ((((2 * n) + 1) * PI) * <i>) = - 1