let n be Element of NAT ; :: thesis: abs ((- 1) |^ n) = 1

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

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

then A1: ex k being Element of NAT st n = 2 * k by ABIAN:def 2;
(- 1) |^ n = (- 1) to_power n by POWER:46
.= 1 to_power n by A1, POWER:54
.= 1 by POWER:31 ;
hence abs ((- 1) |^ n) = 1 by ABSVALUE:def 1; :: thesis: verum

end;

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

then n mod 2 = 1 by NAT_2:24;
then consider k being Nat such that
A2: ( n = (2 * k) + 1 & 1 < 2 ) by NAT_D:def 2;
reconsider k = k as Element of NAT by ORDINAL1:def 13;
A3: ( n = (2 * k) + 1 & 1 < 2 ) by A2;
(- 1) |^ n = (- 1) to_power n by POWER:46
.= - (1 to_power n) by A3, POWER:55
.= - 1 by POWER:31 ;
then abs ((- 1) |^ n) = - (- 1) by ABSVALUE:def 1;
hence abs ((- 1) |^ n) = 1 ; :: thesis: verum

end;

end;