for n being even Integer holds (- 1) to_power n = 1