let X be non empty set ; :: thesis: for S being SigmaField of X
for f being PartFunc of X,COMPLEX
for k being real number
for E being Element of S st 0 <= k & E c= dom f & f is_measurable_on E holds
|.f.| to_power k is_measurable_on E
let S be SigmaField of X; :: thesis: for f being PartFunc of X,COMPLEX
for k being real number
for E being Element of S st 0 <= k & E c= dom f & f is_measurable_on E holds
|.f.| to_power k is_measurable_on E
let f be PartFunc of X,COMPLEX; :: thesis: for k being real number
for E being Element of S st 0 <= k & E c= dom f & f is_measurable_on E holds
|.f.| to_power k is_measurable_on E
let k be real number ; :: thesis: for E being Element of S st 0 <= k & E c= dom f & f is_measurable_on E holds
|.f.| to_power k is_measurable_on E
let E be Element of S; :: thesis: ( 0 <= k & E c= dom f & f is_measurable_on E implies |.f.| to_power k is_measurable_on E )
assume that
A1: 0 <= k and
A2: E c= dom f and
A3: f is_measurable_on E ; :: thesis: |.f.| to_power k is_measurable_on E
A4: |.f.| is nonnegative by Lm1;
E c= dom |.f.| by A2, VALUED_1:def 11;
hence |.f.| to_power k is_measurable_on E by A1, A2, A3, A4, MESFUN6C:29, MESFUN6C:30; :: thesis: verum