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 dom f in S & ( for x being Element of X st x in dom f holds
0 = f . x ) holds
( f is_integrable_on M & Integral (M,f) = 0 )
let S be SigmaField of X; :: thesis: for M being sigma_Measure of S
for f being PartFunc of X,COMPLEX st dom f in S & ( for x being Element of X st x in dom f holds
0 = f . x ) holds
( f is_integrable_on M & Integral (M,f) = 0 )
let M be sigma_Measure of S; :: thesis: for f being PartFunc of X,COMPLEX st dom f in S & ( for x being Element of X st x in dom f holds
0 = f . x ) holds
( f is_integrable_on M & Integral (M,f) = 0 )
let f be PartFunc of X,COMPLEX; :: thesis: ( dom f in S & ( for x being Element of X st x in dom f holds
0 = f . x ) implies ( f is_integrable_on M & Integral (M,f) = 0 ) )
assume dom f in S ; :: thesis: ( ex x being Element of X st
( x in dom f & not 0 = f . x ) or ( f is_integrable_on M & Integral (M,f) = 0 ) )
then reconsider E = dom f as Element of S ;
assume A1: for x being Element of X st x in dom f holds
0 = f . x ; :: thesis: ( f is_integrable_on M & Integral (M,f) = 0 )
A2: for x being Element of X st x in dom f holds
( (Re f) . x = 0 & (Im f) . x = 0 )

proof

let x be Element of X; :: thesis: ( x in dom f implies ( (Re f) . x = 0 & (Im f) . x = 0 ) )
assume A3: x in dom f ; :: thesis: ( (Re f) . x = 0 & (Im f) . x = 0 )
A4: ( x in dom (Re f) & x in dom (Im f) ) by A3, COMSEQ_3:def 3, COMSEQ_3:def 4;
A5: (Re f) . x = Re (f . x) by COMSEQ_3:def 3, A4
.= 0 by A3, A1, COMPLEX1:4 ;
(Im f) . x = Im (f . x) by COMSEQ_3:def 4, A4
.= 0 by A3, A1, COMPLEX1:4 ;
hence ( (Re f) . x = 0 & (Im f) . x = 0 ) by A5; :: thesis: verum

end;

A6: dom (Re f) = E by COMSEQ_3:def 3;
A7: dom (Im f) = E by COMSEQ_3:def 4;
set f1 = Re f;
A8: ( E = dom (Re f) & ( for x being Element of X st x in dom (Re f) holds
0 = (Re f) . x ) ) by A2, A6;
A9: ( R_EAL (Re f) is_integrable_on M & Integral (M,(R_EAL (Re f))) = 0 ) by LPSPACE1:22, A8;
A10: ( Re f is_integrable_on M & Integral (M,(Re f)) = 0 ) by A9;
set f2 = Im f;
A11: ( E = dom (Im f) & ( for x being Element of X st x in dom (Im f) holds
0 = (Im f) . x ) ) by A2, A7;
A12: ( R_EAL (Im f) is_integrable_on M & Integral (M,(R_EAL (Im f))) = 0 ) by LPSPACE1:22, A11;
A13: ( Im f is_integrable_on M & Integral (M,(Im f)) = 0 ) by A12;
f is_integrable_on M by A10, A13, MESFUN6C:def 2;
then ex RF, IF being Real st
( RF = Integral (M,(Re f)) & IF = Integral (M,(Im f)) & Integral (M,f) = RF + (IF * <i>) ) by MESFUN6C:def 3;
hence ( f is_integrable_on M & Integral (M,f) = 0 ) by A10, A13, MESFUN6C:def 2; :: thesis: verum