theorem Th32: :: POWER:32

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