theorem Th53: :: PREPOWER:53

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