let n be Nat; :: thesis: ( n is odd implies (- 1) |^ n = - 1 )
assume A1: n is odd ; :: thesis: (- 1) |^ n = - 1
(- 1) |^ n = (- 1) to_power n by POWER:41;
hence (- 1) |^ n = - 1 by A1, FIB_NUM2:2; :: thesis: verum