theorem :: SIN_COS3:33

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