let a be real number ; :: thesis: for p being Rational st a > 0 & p = 0 holds
a #Q p = 1
let p be Rational; :: thesis: ( a > 0 & p = 0 implies a #Q p = 1 )
assume A1: ( a > 0 & p = 0 ) ; :: thesis: a #Q p = 1
reconsider i = 0 as Integer ;
numerator p = 0 by A1, RAT_1:36;
hence a #Q p = 1 -Root (a #Z i) by A1, RAT_1:42
.= 1 -Root 1 by Th44
.= 1 by Th30 ;
:: thesis: verum