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 ;
R = 0 by ;
then A7: |.(Integral (M,(Re f))).| = 0 by ;
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 ;
A13: now :: thesis: for x being Element of X st x in dom (Re f) holds
|.((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 ;
hence |.((Re f) . x).| <= |.f.| . x by ; :: thesis: verum
end;
Re f is A -measurable by A11;
hence |.(Integral (M,f)).| <= Integral (M,|.f.|) by ; :: thesis: verum