let X be non empty set ; :: thesis: for S being SigmaField of X
for f being PartFunc of X,COMPLEX
for k being Real
for E being Element of S st 0 <= k & E c= dom f & f is E -measurable holds
|.f.| to_power k is E -measurable

let S be SigmaField of X; :: thesis: for f being PartFunc of X,COMPLEX
for k being Real
for E being Element of S st 0 <= k & E c= dom f & f is E -measurable holds
|.f.| to_power k is E -measurable

let f be PartFunc of X,COMPLEX; :: thesis: for k being Real
for E being Element of S st 0 <= k & E c= dom f & f is E -measurable holds
|.f.| to_power k is E -measurable

let k be Real; :: thesis: for E being Element of S st 0 <= k & E c= dom f & f is E -measurable holds
|.f.| to_power k is E -measurable

let E be Element of S; :: thesis: ( 0 <= k & E c= dom f & f is E -measurable implies |.f.| to_power k is E -measurable )
assume that
A1: 0 <= k and
A2: E c= dom f and
A3: f is E -measurable ; :: thesis:
A4: |.f.| is nonnegative by Lm1;
E c= dom |.f.| by ;
hence |.f.| to_power k is E -measurable by ; :: thesis: verum