theorem Th31: :: POWER:31

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