theorem Th19: :: LPSPACE2:19

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