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:45
.= (1 / ((- 1) #Z 1)) #Z (2 * n) by PREPOWER:41
.= (1 / (- 1)) #Z (2 * n) by PREPOWER:35
.= (- 1) |^ (2 * n) by PREPOWER:36
.= 1 |^ (2 * n) by WSIERP_1:2
.= (1 |^ 2) |^ n
.= 1 |^ n
.= 1 ;
hence (- 1) to_power (- (2 * n)) = 1 ; :: thesis: verum