theorem Th28: :: POWER:28

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