theorem :: POWER:30

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)