let X be non empty set ; :: thesis: for S being SigmaField of X

for M being sigma_Measure of S

for f being PartFunc of X,COMPLEX st ex A being Element of S st

( A = dom f & f is A -measurable ) & f is_integrable_on M & Integral (M,f) = 0 holds

|.(Integral (M,f)).| <= Integral (M,|.f.|)

let S be SigmaField of X; :: thesis: for M being sigma_Measure of S

for f being PartFunc of X,COMPLEX st ex A being Element of S st

( A = dom f & f is A -measurable ) & f is_integrable_on M & Integral (M,f) = 0 holds

|.(Integral (M,f)).| <= Integral (M,|.f.|)

let M be sigma_Measure of S; :: thesis: for f being PartFunc of X,COMPLEX st ex A being Element of S st

( A = dom f & f is A -measurable ) & f is_integrable_on M & Integral (M,f) = 0 holds

|.(Integral (M,f)).| <= Integral (M,|.f.|)

let f be PartFunc of X,COMPLEX; :: thesis: ( ex A being Element of S st

( A = dom f & f is A -measurable ) & f is_integrable_on M & Integral (M,f) = 0 implies |.(Integral (M,f)).| <= Integral (M,|.f.|) )

assume that

A1: ex A being Element of S st

( A = dom f & f is A -measurable ) and

A2: f is_integrable_on M and

A3: Integral (M,f) = 0 ; :: thesis: |.(Integral (M,f)).| <= Integral (M,|.f.|)

A4: |.f.| is_integrable_on M by A1, A2, Th31;

consider R, I being Real such that

A5: R = Integral (M,(Re f)) and

I = Integral (M,(Im f)) and

A6: Integral (M,f) = R + (I * <i>) by A2, Def3;

R = 0 by A3, A6, COMPLEX1:4, COMPLEX1:12;

then A7: |.(Integral (M,(Re f))).| = 0 by A5, EXTREAL1:16;

Re f is_integrable_on M by A2;

then A8: |.(Integral (M,(Re f))).| <= Integral (M,|.(Re f).|) by MESFUNC6:95;

A9: dom |.f.| = dom f by VALUED_1:def 11;

consider A being Element of S such that

A10: A = dom f and

A11: f is A -measurable by A1;

A12: dom (Re f) = A by A10, COMSEQ_3:def 3;

hence |.(Integral (M,f)).| <= Integral (M,|.f.|) by A3, A4, A8, A10, A12, A9, A13, A7, COMPLEX1:44, MESFUNC6:96; :: thesis: verum

for M being sigma_Measure of S

for f being PartFunc of X,COMPLEX st ex A being Element of S st

( A = dom f & f is A -measurable ) & f is_integrable_on M & Integral (M,f) = 0 holds

|.(Integral (M,f)).| <= Integral (M,|.f.|)

let S be SigmaField of X; :: thesis: for M being sigma_Measure of S

for f being PartFunc of X,COMPLEX st ex A being Element of S st

( A = dom f & f is A -measurable ) & f is_integrable_on M & Integral (M,f) = 0 holds

|.(Integral (M,f)).| <= Integral (M,|.f.|)

let M be sigma_Measure of S; :: thesis: for f being PartFunc of X,COMPLEX st ex A being Element of S st

( A = dom f & f is A -measurable ) & f is_integrable_on M & Integral (M,f) = 0 holds

|.(Integral (M,f)).| <= Integral (M,|.f.|)

let f be PartFunc of X,COMPLEX; :: thesis: ( ex A being Element of S st

( A = dom f & f is A -measurable ) & f is_integrable_on M & Integral (M,f) = 0 implies |.(Integral (M,f)).| <= Integral (M,|.f.|) )

assume that

A1: ex A being Element of S st

( A = dom f & f is A -measurable ) and

A2: f is_integrable_on M and

A3: Integral (M,f) = 0 ; :: thesis: |.(Integral (M,f)).| <= Integral (M,|.f.|)

A4: |.f.| is_integrable_on M by A1, A2, Th31;

consider R, I being Real such that

A5: R = Integral (M,(Re f)) and

I = Integral (M,(Im f)) and

A6: Integral (M,f) = R + (I * <i>) by A2, Def3;

R = 0 by A3, A6, COMPLEX1:4, COMPLEX1:12;

then A7: |.(Integral (M,(Re f))).| = 0 by A5, EXTREAL1:16;

Re f is_integrable_on M by A2;

then A8: |.(Integral (M,(Re f))).| <= Integral (M,|.(Re f).|) by MESFUNC6:95;

A9: dom |.f.| = dom f by VALUED_1:def 11;

consider A being Element of S such that

A10: A = dom f and

A11: f is A -measurable by A1;

A12: dom (Re f) = A by A10, COMSEQ_3:def 3;

A13: now :: thesis: for x being Element of X st x in dom (Re f) holds

|.((Re f) . x).| <= |.f.| . x

Re f is A -measurable
by A11;|.((Re f) . x).| <= |.f.| . x

let x be Element of X; :: thesis: ( x in dom (Re f) implies |.((Re f) . x).| <= |.f.| . x )

assume A14: x in dom (Re f) ; :: thesis: |.((Re f) . x).| <= |.f.| . x

then A15: (Re f) . x = Re (f . x) by COMSEQ_3:def 3;

|.f.| . x = |.(f . x).| by A10, A12, A9, A14, VALUED_1:def 11;

hence |.((Re f) . x).| <= |.f.| . x by A15, COMPLEX1:79; :: thesis: verum

end;assume A14: x in dom (Re f) ; :: thesis: |.((Re f) . x).| <= |.f.| . x

then A15: (Re f) . x = Re (f . x) by COMSEQ_3:def 3;

|.f.| . x = |.(f . x).| by A10, A12, A9, A14, VALUED_1:def 11;

hence |.((Re f) . x).| <= |.f.| . x by A15, COMPLEX1:79; :: thesis: verum

hence |.(Integral (M,f)).| <= Integral (M,|.f.|) by A3, A4, A8, A10, A12, A9, A13, A7, COMPLEX1:44, MESFUNC6:96; :: thesis: verum