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 ) 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 A -measurable ) 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 A -measurable ) 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 A -measurable ) implies ( f is_integrable_on M iff |.f.| is_integrable_on M ) )

A1: dom (|.(Re f).| + |.(Im f).|) = (dom |.(Re f).|) /\ (dom |.(Im f).|) by VALUED_1:def 1;

A2: dom |.(Re f).| = dom (Re f) by VALUED_1:def 11;

A3: dom |.(Im f).| = dom (Im f) by VALUED_1:def 11;

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

assume ex A being Element of S st

( A = dom f & f is A -measurable ) ; :: thesis: ( f is_integrable_on M iff |.f.| is_integrable_on M )

then consider A being Element of S such that

A5: A = dom f and

A6: f is A -measurable ;

A7: dom (Re f) = A by A5, COMSEQ_3:def 3;

A8: Im f is A -measurable by A6;

A9: Re f is A -measurable by A6;

A10: dom (Im f) = A by A5, COMSEQ_3:def 4;

A11: |.f.| is A -measurable by A5, A6, Th30;

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 ) 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 A -measurable ) 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 A -measurable ) 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 A -measurable ) implies ( f is_integrable_on M iff |.f.| is_integrable_on M ) )

A1: dom (|.(Re f).| + |.(Im f).|) = (dom |.(Re f).|) /\ (dom |.(Im f).|) by VALUED_1:def 1;

A2: dom |.(Re f).| = dom (Re f) by VALUED_1:def 11;

A3: dom |.(Im f).| = dom (Im f) by VALUED_1:def 11;

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

assume ex A being Element of S st

( A = dom f & f is A -measurable ) ; :: thesis: ( f is_integrable_on M iff |.f.| is_integrable_on M )

then consider A being Element of S such that

A5: A = dom f and

A6: f is A -measurable ;

A7: dom (Re f) = A by A5, COMSEQ_3:def 3;

A8: Im f is A -measurable by A6;

A9: Re f is A -measurable by A6;

A10: dom (Im f) = A by A5, COMSEQ_3:def 4;

A11: |.f.| is A -measurable by A5, A6, Th30;

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

then Im f is_integrable_on M ;

then A20: |.(Im f).| is_integrable_on M by A10, A8, MESFUNC6:94;

Re f is_integrable_on M by A19;

then |.(Re f).| is_integrable_on M by A7, A9, MESFUNC6:94;

then |.(Re f).| + |.(Im f).| is_integrable_on M by A20, MESFUNC6:100;

hence |.f.| is_integrable_on M by A5, A7, A10, A1, A2, A3, A4, A11, A12, MESFUNC6:96; :: thesis: verum

end;

A12: now :: thesis: for x being Element of X st x in dom |.f.| holds

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

assume A19:
f is_integrable_on M
; :: thesis: |.f.| is_integrable_on M|.(|.f.| . x).| <= (|.(Re f).| + |.(Im f).|) . x

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

assume A13: x in dom |.f.| ; :: thesis: |.(|.f.| . x).| <= (|.(Re f).| + |.(Im f).|) . x

then A14: |.f.| . x = |.(f . x).| by VALUED_1:def 11;

A15: |.((Im f) . x).| = |.(Im f).| . x by A5, A10, A3, A4, A13, VALUED_1:def 11;

A16: |.((Re f) . x).| = |.(Re f).| . x by A5, A7, A2, A4, A13, VALUED_1:def 11;

A17: (Im f) . x = Im (f . x) by A5, A10, A4, A13, COMSEQ_3:def 4;

A18: (Re f) . x = Re (f . x) by A5, A7, A4, A13, COMSEQ_3:def 3;

(|.(Re f).| + |.(Im f).|) . x = (|.(Re f).| . x) + (|.(Im f).| . x) by A5, A7, A10, A1, A2, A3, A4, A13, VALUED_1:def 1;

hence |.(|.f.| . x).| <= (|.(Re f).| + |.(Im f).|) . x by A18, A17, A14, A16, A15, COMPLEX1:78; :: thesis: verum

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

then A14: |.f.| . x = |.(f . x).| by VALUED_1:def 11;

A15: |.((Im f) . x).| = |.(Im f).| . x by A5, A10, A3, A4, A13, VALUED_1:def 11;

A16: |.((Re f) . x).| = |.(Re f).| . x by A5, A7, A2, A4, A13, VALUED_1:def 11;

A17: (Im f) . x = Im (f . x) by A5, A10, A4, A13, COMSEQ_3:def 4;

A18: (Re f) . x = Re (f . x) by A5, A7, A4, A13, COMSEQ_3:def 3;

(|.(Re f).| + |.(Im f).|) . x = (|.(Re f).| . x) + (|.(Im f).| . x) by A5, A7, A10, A1, A2, A3, A4, A13, VALUED_1:def 1;

hence |.(|.f.| . x).| <= (|.(Re f).| + |.(Im f).|) . x by A18, A17, A14, A16, A15, COMPLEX1:78; :: thesis: verum

then Im f is_integrable_on M ;

then A20: |.(Im f).| is_integrable_on M by A10, A8, MESFUNC6:94;

Re f is_integrable_on M by A19;

then |.(Re f).| is_integrable_on M by A7, A9, MESFUNC6:94;

then |.(Re f).| + |.(Im f).| is_integrable_on M by A20, MESFUNC6:100;

hence |.f.| is_integrable_on M by A5, A7, A10, A1, A2, A3, A4, A11, A12, MESFUNC6:96; :: thesis: verum

hereby :: thesis: verum

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

hence f is_integrable_on M by A24; :: thesis: verum

end;now :: thesis: for x being Element of X st x in dom (Im f) holds

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

then A24:
Im f is_integrable_on M
by A5, A10, A8, A4, A21, MESFUNC6:96;|.((Im f) . x).| <= |.f.| . x

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

A22: |.(Im (f . x)).| <= |.(f . x).| by COMPLEX1:79;

assume A23: x in dom (Im f) ; :: thesis: |.((Im f) . x).| <= |.f.| . x

then |.f.| . x = |.(f . x).| by A5, A10, A4, VALUED_1:def 11;

hence |.((Im f) . x).| <= |.f.| . x by A23, A22, COMSEQ_3:def 4; :: thesis: verum

end;A22: |.(Im (f . x)).| <= |.(f . x).| by COMPLEX1:79;

assume A23: x in dom (Im f) ; :: thesis: |.((Im f) . x).| <= |.f.| . x

then |.f.| . x = |.(f . x).| by A5, A10, A4, VALUED_1:def 11;

hence |.((Im f) . x).| <= |.f.| . x by A23, A22, COMSEQ_3:def 4; :: thesis: verum

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

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

then
Re f is_integrable_on M
by A5, A7, A9, A4, A21, MESFUNC6:96;|.((Re f) . x).| <= |.f.| . x

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

A25: |.(Re (f . x)).| <= |.(f . x).| by COMPLEX1:79;

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

then |.f.| . x = |.(f . x).| by A5, A7, A4, VALUED_1:def 11;

hence |.((Re f) . x).| <= |.f.| . x by A26, A25, COMSEQ_3:def 3; :: thesis: verum

end;A25: |.(Re (f . x)).| <= |.(f . x).| by COMPLEX1:79;

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

then |.f.| . x = |.(f . x).| by A5, A7, A4, VALUED_1:def 11;

hence |.((Re f) . x).| <= |.f.| . x by A26, A25, COMSEQ_3:def 3; :: thesis: verum

hence f is_integrable_on M by A24; :: thesis: verum