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

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

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

then reconsider n = n as odd 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;

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 Th5
.= (- 1) to_power n by Th5 ;
hence (- 1) to_power (- n) = (- 1) to_power n ; :: thesis: verum

end;

end;