theorem Th18: :: LPSPACE2:18

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