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

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

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

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

end;

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

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

end;

end;