theorem Th58: :: PREPOWER:58
for a, b being Real
for p being Rational st a > 0 & b > 0 holds
(a / b) #Q p = (a #Q p) / (b #Q p)