let n be even Integer; :: thesis: (- 1) to_power n = 1
(- 1) to_power n = 1 to_power n by POWER:54;
hence (- 1) to_power n = 1 by POWER:31; :: thesis: verum