let n be Nat; :: thesis: (- 1) to_power (- (2 * n)) = 1
(- 1) to_power (- (2 * n)) = (- 1) #Z ((- 1) * (2 * n)) by POWER:def 2
.= ((- 1) #Z (- 1)) #Z (2 * n) by PREPOWER:55
.= (1 / ((- 1) #Z 1)) #Z (2 * n) by PREPOWER:51
.= (1 / (- 1)) #Z (2 * n) by PREPOWER:45
.= (- 1) |^ (2 * n) by PREPOWER:46
.= 1 |^ (2 * n) by WSIERP_1:3
.= (1 |^ 2) |^ n by NEWTON:14
.= 1 |^ n by NEWTON:15
.= 1 by NEWTON:15 ;
hence (- 1) to_power (- (2 * n)) = 1 ; :: thesis: verum