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