theorem Th56: :: PREPOWER:56

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)