let n be odd Integer; :: thesis: (- 1) to_power n = - 1
(- 1) to_power n = - (1 to_power n) by POWER:48
.= - 1 by POWER:26 ;
hence (- 1) to_power n = - 1 ; :: thesis: verum