let a be Real; :: thesis: for p being Rational st a > 0 holds
a to_power p = a #Q p
let p be Rational; :: thesis: ( a > 0 implies a to_power p = a #Q p )
assume A1: a > 0 ; :: thesis: a to_power p = a #Q p
hence a to_power p = a #R p by Def2
.= a #Q p by A1, PREPOWER:74 ;
:: thesis: verum