let n be Nat; :: thesis: (- tau) to_power ((- 1) * n) = ((- tau) to_power (- 1)) to_power n
(- tau) to_power ((- 1) * n) = (- tau) #Z ((- 1) * n) by POWER:def 2
.= ((- tau) #Z (- 1)) #Z n by PREPOWER:55
.= (1 / ((- tau) #Z 1)) #Z n by PREPOWER:51
.= (1 / (- tau)) #Z n by PREPOWER:45
.= (1 / (- tau)) to_power n by POWER:def 2
.= ((1 / (- tau)) to_power 1) to_power n by POWER:30
.= ((1 / (- tau)) #Z 1) to_power n by POWER:def 2
.= (1 / ((- tau) #Z 1)) to_power n by PREPOWER:52
.= ((- tau) #Z (- 1)) to_power n by PREPOWER:51 ;
hence (- tau) to_power ((- 1) * n) = ((- tau) to_power (- 1)) to_power n by POWER:def 2; :: thesis: verum