let n be Nat; :: thesis: (- 1) to_power (- n) = (- 1) to_power n

per cases ( n is odd or n is even ) ;

suppose n is odd ; :: thesis: (- 1) to_power (- n) = (- 1) to_power n

then reconsider n = n as odd Integer ;
(- 1) to_power (- n) = - 1 by Th2
.= (- 1) to_power n by Th2 ;
hence (- 1) to_power (- n) = (- 1) to_power n ; :: thesis: verum

end;

suppose n is even ; :: thesis: (- 1) to_power (- n) = (- 1) to_power n

then reconsider n = n as even Integer ;
(- 1) to_power (- n) = 1 by Th3
.= (- 1) to_power n by Th3 ;
hence (- 1) to_power (- n) = (- 1) to_power n ; :: thesis: verum

end;

end;