let n be Nat; :: thesis: |.((- 1) |^ n).| = 1

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

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

(- 1) |^ n = (- 1) to_power n by POWER:41
.= 1 to_power n by A1, POWER:47
.= 1 by POWER:26 ;
hence |.((- 1) |^ n).| = 1 by ABSVALUE:def 1; :: thesis: verum

end;

suppose A2: n is odd ; :: thesis: |.((- 1) |^ n).| = 1

(- 1) |^ n = (- 1) to_power n by POWER:41
.= - (1 to_power n) by A2, POWER:48
.= - 1 by POWER:26 ;
then |.((- 1) |^ n).| = - (- 1) by ABSVALUE:def 1;
hence |.((- 1) |^ n).| = 1 ; :: thesis: verum

end;

end;