let a be Real; :: thesis: for p being Rational st p = 0 holds
a #Q p = 1
let p be Rational; :: thesis: ( p = 0 implies a #Q p = 1 )
reconsider i = 0 as Integer ;
assume A1: p = 0 ; :: thesis: a #Q p = 1
numerator p = 0 by A1, RAT_1:14;
hence a #Q p = 1 -Root (a #Z i) by A1, RAT_1:19
.= 1 -Root 1 by Th34
.= 1 by Th21 ;
:: thesis: verum