theorem Th44: :: POWER:44
for a being Real
for p being Rational st a > 0 holds
a to_power p = a #Q p