let n be Nat; :: thesis: ( not n is even implies (- 1) |^ n = - 1 )
assume A1: not n is even ; :: thesis: (- 1) |^ n = - 1
reconsider n = n as Element of NAT by ORDINAL1:def 12;
(- 1) |^ n = (- 1) to_power n by POWER:41;
hence (- 1) |^ n = - 1 by A1, FIB_NUM2:2; :: thesis: verum