theorem Th57: :: PREPOWER:57
for a being Real
for p being Rational st a > 0 holds
(1 / a) #Q p = 1 / (a #Q p)