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

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 13;
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

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

end;

end;