let a be real number ; :: thesis: for p being Rational
for n being Nat st a > 0 & n >= 1 & p = n " holds
a #Q p = n -Root a
let p be Rational; :: thesis: for n being Nat st a > 0 & n >= 1 & p = n " holds
a #Q p = n -Root a
let n be Nat; :: thesis: ( a > 0 & n >= 1 & p = n " implies a #Q p = n -Root a )
assume A1: ( a > 0 & n >= 1 & p = n " ) ; :: thesis: a #Q p = n -Root a
then A2: p = 1 / n ;
reconsider q = n as Rational ;
( numerator p = denominator q & denominator p = numerator q ) by A1, A2, RAT_1:88;
then ( numerator p = 1 & denominator p = n ) by RAT_1:40;
hence a #Q p = n -Root a by Th45; :: thesis: verum