let n be Nat; :: thesis: ((- 1) to_power (- n)) ^2 = 1
((- 1) to_power (- n)) ^2 = ((- 1) #Z (- n)) ^2 by POWER:def 2
.= (1 / ((- 1) #Z n)) ^2 by PREPOWER:41
.= (1 / ((- 1) #Z n)) to_power 2 by POWER:46
.= (1 / ((- 1) #Z n)) |^ 2 by POWER:41
.= 1 / (((- 1) #Z n) |^ 2) by PREPOWER:7
.= 1 / (((- 1) #Z n) #Z 2) by PREPOWER:36
.= 1 / ((- 1) #Z (n * 2)) by PREPOWER:45
.= 1 / ((- 1) |^ (2 * n)) by PREPOWER:36
.= 1 / (1 |^ (2 * n)) by WSIERP_1:2
.= 1 / ((1 |^ 2) |^ n)
.= 1 / (1 |^ n)
.= 1 / 1 ;
hence ((- 1) to_power (- n)) ^2 = 1 ; :: thesis: verum