theorem :: HOLDER_1:2

for p, q being Real st 0 < p & 0 < q holds
for a being Real st 0 <= a holds
(a to_power p) to_power q = a to_power (p * q)