theorem :: HOLDER_1:1

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