theorem Th7: :: LPSPACE2:7

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) (#) (f to_power b) = f to_power (a + b)