theorem Th6: :: LPSPACE2:6

for X being non empty set
for a, b being Real
for f being PartFunc of X,REAL st f is nonnegative & a > 0 & b > 0 holds
(f to_power a) to_power b = f to_power (a * b)