theorem Th33: :: POWER:33

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