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