let a be real number ; :: thesis: for n being Nat st 0 <= a holds
a #Q n = a |^ n
let n be Nat; :: thesis: ( 0 <= a implies a #Q n = a |^ n )
assume A1: 0 <= a ; :: thesis: a #Q n = a |^ n
( denominator n = 1 & numerator n = n ) by RAT_1:40;
hence a #Q n = a #Z n by Th30, A1, Lm49
.= a |^ n by Th46 ;
:: thesis: verum