theorem Th20: :: LPSPACE2:20

for X being non empty set
for f being PartFunc of X,REAL
for k being Real
for E being set holds (f | E) to_power k = (f to_power k) | E