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