let n be Nat; :: thesis: (- 1) |^ n is Integer

per cases ( n is even or n is odd ) ;

suppose n is even ; :: thesis: (- 1) |^ n is Integer

hence (- 1) |^ n is Integer by Th8; :: thesis: verum

end;

suppose n is odd ; :: thesis: (- 1) |^ n is Integer

hence (- 1) |^ n is Integer by Th9; :: thesis: verum

end;

end;