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