consider b being Element of NAT such that
A1: ( a = b or a = - b ) by INT_1:2;

per cases ( a = b or a = - b ) by A1;

suppose a = b ; :: thesis: a |^ n is Element of INT

then reconsider a = a as Element of NAT ;
reconsider s = a |^ n as Element of NAT by ORDINAL1:def 12;
s in NAT ;
hence a |^ n is Element of INT by NUMBERS:17; :: thesis: verum

end;

suppose A2: a = - b ; :: thesis: a |^ n is Element of INT

reconsider bn = b |^ n as Element of NAT by ORDINAL1:def 12;
(- 1) |^ n is Integer by Th10;
then reconsider l = (- 1) |^ n as Element of INT by INT_1:def 2;
- b = (- 1) * b ;
then a |^ n = l * bn by A2, NEWTON:7;
hence a |^ n is Element of INT ; :: thesis: verum

end;

end;