let n be Nat; :: thesis: (- 1) |^ n = (- 1) |^ (n + 2)
(- 1) |^ (n + 2) = ((- 1) |^ n) * ((- 1) |^ 2) by NEWTON:8
.= (- 1) |^ n by Th11 ;
hence (- 1) |^ n = (- 1) |^ (n + 2) ; :: thesis: verum