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:45
.= (1 / ((- tau) #Z 1)) #Z n by PREPOWER:41
.= (1 / (- tau)) #Z n by PREPOWER:35
.= (1 / (- tau)) to_power n by POWER:def 2
.= ((1 / (- tau)) to_power 1) to_power n by POWER:25
.= ((1 / (- tau)) #Z 1) to_power n by POWER:def 2
.= (1 / ((- tau) #Z 1)) to_power n by PREPOWER:42
.= ((- tau) #Z (- 1)) to_power n by PREPOWER:41 ;
hence (- tau) to_power ((- 1) * n) = ((- tau) to_power (- 1)) to_power n by POWER:def 2; :: thesis: verum