let X be non empty set ; :: thesis:
let S be SigmaField of X; :: thesis:
let M be sigma_Measure of S; :: thesis:
let f be PartFunc of X,COMPLEX ; :: thesis:
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
X1: Integral M,f = 0 ; :: thesis:
D1: |.f.| is_integrable_on M by A1, A2, Th94;
consider R, I being Real such that
A3: ( R = Integral M,(Re f) & I = Integral M,(Im f) & Integral M,f = R + (I * <i> ) ) by A2, Def5;
Re f is_integrable_on M by A2, Def4;
then C1: |.(Integral M,(Re f)).| <= Integral M,|.(Re f).| by MESFUNC6:95;
consider A being Element of S such that
A4: ( A = dom f & f is_measurable_on A ) by A1;
B1: ( dom (Re f) = A & Re f is_measurable_on A ) by A4, Def1, Def3;
A5: dom |.f.| = dom f by VALUED_1:def 11;

C2: now

let x be Element of X; :: thesis:
assume x in dom (Re f) ; :: thesis:
then ( (Re f) . x = Re (f . x) & |.f.| . x = |.(f . x).| ) by A5, B1, A4, Def1, VALUED_1:def 11;
hence |.((Re f) . x).| <= |.f.| . x by COMPLEX1:165; :: thesis:

end;