theorem Th50: :: PREPOWER:50
for a being Real
for p being Rational
for n being Nat st n >= 1 & p = n " holds
a #Q p = n -Root a