let a be real number ; :: thesis: for l being Integer st a > 0 holds
a #Q l = a #Z l
let l be Integer; :: thesis: ( a > 0 implies a #Q l = a #Z l )
assume a > 0 ; :: thesis: a #Q l = a #Z l
then a #Z l > 0 by Th49;
then A: a #Z l = (1 -Root (a #Z l)) |^ 1 by Def3;
( denominator l = 1 & numerator l = l ) by RAT_1:40;
hence a #Q l = 1 -Root (a #Z l)
.= a #Z l by A, NEWTON:10 ;
:: thesis: verum