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 ) holds
( f is_integrable_on M iff |.f.| is_integrable_on M )
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 ) holds
( f is_integrable_on M iff |.f.| is_integrable_on M )
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 ) holds
( f is_integrable_on M iff |.f.| is_integrable_on M )
let f be PartFunc of X,COMPLEX ; :: thesis: ( ex A being Element of S st
( A = dom f & f is_measurable_on A ) implies ( f is_integrable_on M iff |.f.| is_integrable_on M ) )
assume ex A being Element of S st
( A = dom f & f is_measurable_on A ) ; :: thesis: ( f is_integrable_on M iff |.f.| is_integrable_on M )
then consider A being Element of S such that
P1: ( A = dom f & f is_measurable_on A ) ;
P2: ( dom (Re f) = A & dom (Im f) = A ) by P1, Def1, Def2;
P3: ( Re f is_measurable_on A & Im f is_measurable_on A ) by Def3, P1;
P5: dom (|.(Re f).| + |.(Im f).|) = (dom |.(Re f).|) /\ (dom |.(Im f).|) by VALUED_1:def 1;
P4: ( dom |.(Re f).| = dom (Re f) & dom |.(Im f).| = dom (Im f) & dom |.f.| = dom f ) by VALUED_1:def 11;
P7: |.f.| is_measurable_on A by MES648, P1;

hereby :: thesis: ( |.f.| is_integrable_on M implies f is_integrable_on M )

assume f is_integrable_on M ; :: thesis: |.f.| is_integrable_on M
then ( Re f is_integrable_on M & Im f is_integrable_on M ) by Def4;
then ( |.(Re f).| is_integrable_on M & |.(Im f).| is_integrable_on M ) by P2, P3, MESFUNC6:94;
then L9: |.(Re f).| + |.(Im f).| is_integrable_on M by MESFUNC6:100;

now

let x be Element of X; :: thesis: ( x in dom |.f.| implies |.(|.f.| . x).| <= (|.(Re f).| + |.(Im f).|) . x )
assume P11: x in dom |.f.| ; :: thesis: |.(|.f.| . x).| <= (|.(Re f).| + |.(Im f).|) . x
then P14: ( (Re f) . x = Re (f . x) & (Im f) . x = Im (f . x) ) by P1, P2, P4, Def1, Def2;
P15: |.f.| . x = |.(f . x).| by P11, VALUED_1:def 11;
( |.((Re f) . x).| = |.(Re f).| . x & |.((Im f) . x).| = |.(Im f).| . x & (|.(Re f).| + |.(Im f).|) . x = (|.(Re f).| . x) + (|.(Im f).| . x) ) by P1, P2, P11, P4, P5, VALUED_1:def 1, VALUED_1:def 11;
hence |.(|.f.| . x).| <= (|.(Re f).| + |.(Im f).|) . x by P14, P15, COMPLEX1:164; :: thesis: verum

end;

hence |.f.| is_integrable_on M by P1, P7, P4, L9, P5, P2, MESFUNC6:96; :: thesis: verum

end;

hereby :: thesis: verum

assume R: |.f.| is_integrable_on M ; :: thesis: f is_integrable_on M

now

let x be Element of X; :: thesis: ( x in dom (Re f) implies |.((Re f) . x).| <= |.f.| . x )
assume P101: x in dom (Re f) ; :: thesis: |.((Re f) . x).| <= |.f.| . x
then P13: |.f.| . x = |.(f . x).| by P1, P2, P4, VALUED_1:def 11;
|.(Re (f . x)).| <= |.(f . x).| by COMPLEX1:165;
hence |.((Re f) . x).| <= |.f.| . x by P13, P101, Def1; :: thesis: verum

end;

then R11: Re f is_integrable_on M by P2, P3, P4, P1, R, MESFUNC6:96;

now

let x be Element of X; :: thesis: ( x in dom (Im f) implies |.((Im f) . x).| <= |.f.| . x )
assume P101: x in dom (Im f) ; :: thesis: |.((Im f) . x).| <= |.f.| . x
then P14: |.f.| . x = |.(f . x).| by P1, P2, P4, VALUED_1:def 11;
|.(Im (f . x)).| <= |.(f . x).| by COMPLEX1:165;
hence |.((Im f) . x).| <= |.f.| . x by P14, P101, Def2; :: thesis: verum

end;

then Im f is_integrable_on M by P2, P3, P4, P1, R, MESFUNC6:96;
hence f is_integrable_on M by Def4, R11; :: thesis: verum

end;