let a be Real; :: 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 Th39;
then A1: a #Z l = (1 -Root (a #Z l)) |^ 1 by Def2;
denominator l = 1 by RAT_1:17;
hence a #Q l = 1 -Root (a #Z l) by RAT_1:17
.= a #Z l by A1 ;
:: thesis: verum