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

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

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

(- 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 B1: not n is even ; :: thesis: abs ((- 1) |^ n) = 1

consider k being Nat;
reconsider k = k as Element of NAT by ORDINAL1:def 13;
(- 1) |^ n = (- 1) to_power n by POWER:46
.= - (1 to_power n) by B1, POWER:55
.= - 1 by POWER:31 ;
then abs ((- 1) |^ n) = - (- 1) by ABSVALUE:def 1;
hence abs ((- 1) |^ n) = 1 ; :: thesis: verum

end;

end;