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_measurable_on A ) & 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_measurable_on A ) & 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_measurable_on A ) & 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_measurable_on A ) & 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_measurable_on A ) 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, Def5;
R = 0 by A3, A6, COMPLEX1:12, COMPLEX1:28;
then A7: |.(Integral M,(Re f)).| = 0 by A5, EXTREAL2:53;
Re f is_integrable_on M by A2, Def4;
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_measurable_on A by A1;
A12: dom (Re f) = A by A10, COMSEQ_3:def 3;

A13: now

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:165; :: thesis: verum

end;

Re f is_measurable_on A by A11, Def3;
hence |.(Integral M,f).| <= Integral M,|.f.| by A3, A4, A8, A10, A12, A9, A13, A7, COMPLEX1:130, MESFUNC6:96; :: thesis: verum