let a be Real; :: 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 )
A1: denominator n = 1 by RAT_1:17;
A2: numerator n = n by RAT_1:17;
assume 0 <= a ; :: thesis: a #Q n = a |^ n
hence a #Q n = a #Z n by A1, A2, Lm5, Th21
.= a |^ n by Th36 ;
:: thesis: verum