theorem Th59: :: PREPOWER:59

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