theorem Th29: :: POWER:29

for a, b, c being Real st a > 0 holds
a to_power (b - c) = (a to_power b) / (a to_power c)