let x be Real; :: thesis: ( x > 0 implies 1 / x = x to_power (- 1) )
assume x > 0 ; :: thesis: 1 / x = x to_power (- 1)
then x to_power (- 1) = (1 / x) to_power 1 by POWER:32
.= 1 / x by POWER:25 ;
hence 1 / x = x to_power (- 1) ; :: thesis: verum