let a, b be Real; :: thesis: ( a > 0 implies (1 / a) to_power b = a to_power (- b) )
assume A1: a > 0 ; :: thesis: (1 / a) to_power b = a to_power (- b)
hence (1 / a) to_power b = (1 / a) #R b by Def2
.= 1 / (a #R b) by A1, PREPOWER:79
.= 1 / (a to_power b) by A1, Def2
.= a to_power (- b) by A1, Th28 ;
:: thesis: verum