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

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