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 f in L1_CFunctions M & Integral (M,(abs f)) = 0 holds
f a.e.cpfunc= X --> 0c,M
let S be SigmaField of X; :: thesis: for M being sigma_Measure of S
for f being PartFunc of X,COMPLEX st f in L1_CFunctions M & Integral (M,(abs f)) = 0 holds
f a.e.cpfunc= X --> 0c,M
let M be sigma_Measure of S; :: thesis: for f being PartFunc of X,COMPLEX st f in L1_CFunctions M & Integral (M,(abs f)) = 0 holds
f a.e.cpfunc= X --> 0c,M
let f be PartFunc of X,COMPLEX; :: thesis: ( f in L1_CFunctions M & Integral (M,(abs f)) = 0 implies f a.e.cpfunc= X --> 0c,M )
assume that
A1: f in L1_CFunctions M and
A2: Integral (M,(abs f)) = 0 ; :: thesis: f a.e.cpfunc= X --> 0c,M
A3: ex f1 being PartFunc of X,COMPLEX st
( f = f1 & ex ND being Element of S st
( M . ND = 0 & dom f1 = ND ` & f1 is_integrable_on M ) ) by A1;
then consider NDf being Element of S such that
A4: M . NDf = 0 and
A5: dom f = NDf ` and
f is_integrable_on M ;
( dom (abs f) = NDf ` & abs f is_integrable_on M ) by A3, A5, Th37, VALUED_1:def 11;
then A6: abs f in L1_Functions M by A4;
A7: Integral (M,(abs (abs f))) = 0 by A2;
consider Ef being Element of S such that
A8: M . Ef = 0 and
A9: (abs f) | (Ef `) = (X --> 0) | (Ef `) by A6, A7, LPSPACE1:53, LPSPACE1:def 10;
A10: dom (X --> 0) = X by FUNCOP_1:13;
A11: dom ((abs f) | (Ef `)) = (dom (abs f)) /\ (Ef `) by RELAT_1:61;
A12: dom (f | (Ef `)) = (dom f) /\ (Ef `) by RELAT_1:61
.= (dom (abs f)) /\ (Ef `) by VALUED_1:def 11
.= dom ((abs f) | (Ef `)) by RELAT_1:61 ;
for x being object st x in dom (f | (Ef `)) holds
(f | (Ef `)) . x = ((X --> 0) | (Ef `)) . x

proof

let x be object ; :: thesis: ( x in dom (f | (Ef `)) implies (f | (Ef `)) . x = ((X --> 0) | (Ef `)) . x )
assume A13: x in dom (f | (Ef `)) ; :: thesis: (f | (Ef `)) . x = ((X --> 0) | (Ef `)) . x
A14: ( x in dom (abs f) & x in Ef ` ) by A13, A12, A11, XBOOLE_0:def 4;
A15: x in dom ((X --> 0) | (Ef `)) by A10, RELAT_1:62, A14;
A16: (abs f) . x = ((X --> 0) | (Ef `)) . x by A9, A13, A12, FUNCT_1:47
.= (X --> 0) . x by A15, FUNCT_1:47
.= 0 by A13, FUNCOP_1:7 ;
A17: ( (Re (f . x)) ^2 >= 0 & (Im (f . x)) ^2 >= 0 ) by XREAL_1:63;
sqrt (((Re (f . x)) ^2) + ((Im (f . x)) ^2)) = |.(f . x).| by COMPLEX1:def 12
.= 0 by A16, A14, VALUED_1:def 11 ;
then ( (Re (f . x)) ^2 = 0 & (Im (f . x)) ^2 = 0 ) by A17, SQUARE_1:31;
then A18: ((Re (f . x)) ^2) + ((Im (f . x)) ^2) = 0 ;
(f | (Ef `)) . x = f . x by A13, FUNCT_1:47
.= 0 by A18, COMPLEX1:5
.= (X --> 0) . x by A13, FUNCOP_1:7
.= ((X --> 0) | (Ef `)) . x by A15, FUNCT_1:47 ;
hence (f | (Ef `)) . x = ((X --> 0) | (Ef `)) . x ; :: thesis: verum

end;

hence f a.e.cpfunc= X --> 0c,M by A8, A9, A12, FUNCT_1:def 11; :: thesis: verum