theorem Th29: :: MESFUN6C:29

for k being Real
for X being non empty set
for S being SigmaField of X
for E being Element of S
for f being PartFunc of X,REAL st f is nonnegative & 0 <= k & E c= dom f & f is E -measurable holds
f to_power k is E -measurable