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: |.f.| to_power k is E -measurable
A4: |.f.| is nonnegative by Lm1;
E c= dom |.f.| by A2, VALUED_1:def 11;
hence |.f.| to_power k is E -measurable by A1, A2, A3, A4, MESFUN6C:29, MESFUN6C:30; :: thesis: verum