let a be real number ; :: thesis: for p being Rational st a > 0 & p = 1 holds
a #Q p = a
let p be Rational; :: thesis: ( a > 0 & p = 1 implies a #Q p = a )
assume A1: ( a > 0 & p = 1 ) ; :: thesis: a #Q p = a
( numerator p = p & denominator p = 1 ) by A1, RAT_1:40;
hence a #Q p = 1 -Root a by A1, Th45
.= a by A1, Th30 ;
:: thesis: verum