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