theorem Th55: :: PREPOWER:55

for a being Real
for p, q being Rational st a > 0 holds
(a #Q p) / (a #Q q) = a #Q (p - q)