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,REAL st f in L1_Functions M & Integral M,(abs f) = 0 holds
f a.e.= X --> 0 ,M
let S be SigmaField of X; :: thesis: for M being sigma_Measure of S
for f being PartFunc of X,REAL st f in L1_Functions M & Integral M,(abs f) = 0 holds
f a.e.= X --> 0 ,M
let M be sigma_Measure of S; :: thesis: for f being PartFunc of X,REAL st f in L1_Functions M & Integral M,(abs f) = 0 holds
f a.e.= X --> 0 ,M
let f be PartFunc of X,REAL ; :: thesis: ( f in L1_Functions M & Integral M,(abs f) = 0 implies f a.e.= X --> 0 ,M )
assume A1: ( f in L1_Functions M & Integral M,(abs f) = 0 ) ; :: thesis: f a.e.= X --> 0 ,M
then consider f1 being PartFunc of X,REAL such that
A2: ( f = f1 & ex ND being Element of S st
( M . ND = 0 & dom f1 = ND ` & f1 is_integrable_on M ) ) ;
consider ND being Element of S such that
A3: ( M . ND = 0 & dom f1 = ND ` & f1 is_integrable_on M ) by A2;
A4: abs f is_integrable_on M by Lm15, A2;
then R_EAL (abs f) is_integrable_on M by MESFUNC6:def 9;
then consider E being Element of S such that
A5: ( E = dom (R_EAL (abs f)) & R_EAL (abs f) is_measurable_on E ) by MESFUNC5:def 17;
A6: ( E = dom (abs f) & abs f is_measurable_on E ) by A5, MESFUNC6:def 6;

now

let x be set ; :: thesis: ( x in dom (abs f) implies 0 <= (abs f) . x )
assume x in dom (abs f) ; :: thesis: 0 <= (abs f) . x
then (abs f) . x = abs (f . x) by VALUED_1:def 11;
hence 0 <= (abs f) . x by COMPLEX1:132; :: thesis: verum

end;

then A7: abs f is nonnegative by MESFUNC6:52;
defpred S₁[ Element of NAT , set ] means ( $2 = great_eq_dom (abs f),(1 / ($1 + 1)) & M . $2 = 0 );

A8: now

let n be Element of NAT ; :: thesis: ex B being Element of S st S₁[n,B]
set r = 1 / (n + 1);
reconsider Br = E /\ (great_eq_dom (abs f),(1 / (n + 1))) as Element of S by A6, MESFUNC6:13;
A9: Integral M,((abs f) | Br) <= Integral M,((abs f) | E) by A6, A7, MESFUNC6:87, XBOOLE_1:17;
set g = Br --> (1 / (n + 1));
A10: dom (Br --> (1 / (n + 1))) = Br by FUNCT_2:def 1;
A11: for x being set st x in dom (Br --> (1 / (n + 1))) holds
(Br --> (1 / (n + 1))) . x = 1 / (n + 1) by FUNCOP_1:13;
reconsider g = Br --> (1 / (n + 1)) as PartFunc of X,REAL by RELSET_1:17;
A12: g is_measurable_on Br by A10, A11, Lm261a;
for x being set st x in dom g holds
0 <= g . x by A11;
then A13: g is nonnegative by MESFUNC6:52;
dom ((abs f) | Br) = (dom (abs f)) /\ Br by RELAT_1:90
.= Br by A5, XBOOLE_1:17, XBOOLE_1:28 ;
then A14: ( dom g = dom ((abs f) | Br) & (abs f) | Br is_integrable_on M ) by A4, FUNCT_2:def 1, MESFUNC6:91;
for x being set st x in great_eq_dom (abs f),(1 / (n + 1)) holds
x in dom (abs f) by MESFUNC6:6;
then A15: great_eq_dom (abs f),(1 / (n + 1)) c= E by A5, TARSKI:def 3;

now

let x be Element of X; :: thesis: ( x in dom g implies abs (g . x) <= ((abs f) | Br) . x )
assume A16: x in dom g ; :: thesis: abs (g . x) <= ((abs f) | Br) . x
then abs (g . x) = abs (1 / (n + 1)) by A11;
then A17: abs (g . x) = 1 / (n + 1) by ABSVALUE:def 1;
x in E /\ (great_eq_dom (abs f),(1 / (n + 1))) by A16, FUNCT_2:def 1;
then x in great_eq_dom (abs f),(1 / (n + 1)) by XBOOLE_0:def 4;
then ex y being Real st
( y = (abs f) . x & 1 / (n + 1) <= y ) by MESFUNC6:6;
hence abs (g . x) <= ((abs f) | Br) . x by A14, A16, A17, FUNCT_1:70; :: thesis: verum

end;

then A19: Integral M,(abs g) <= Integral M,((abs f) | Br) by A12, A14, A10, MESFUNC6:96;
A20: dom (abs g) = dom g by VALUED_1:def 11;

now

let x be Element of X; :: thesis: ( x in dom (abs g) implies (abs g) . x = g . x )
assume A22: x in dom (abs g) ; :: thesis: (abs g) . x = g . x
then (abs g) . x = abs (g . x) by VALUED_1:def 11;
then (abs g) . x = abs (1 / (n + 1)) by A11, A20, A22;
then (abs g) . x = 1 / (n + 1) by ABSVALUE:def 1;
hence (abs g) . x = g . x by A11, A20, A22; :: thesis: verum

end;

then A23: Integral M,g <= Integral M,((abs f) | Br) by A19, A20, PARTFUN1:34;
0 <= Integral M,g by A10, A11, Lm261a, A13, MESFUNC6:84;
then A25: Integral M,g = 0 by A9, A5, A1, A23, RELAT_1:97;
( 0 <= 1 / (n + 1) & dom g in S & 1 / (n + 1) is Real & ( for x being set st x in dom g holds
g . x = 1 / (n + 1) ) ) by A10, FUNCOP_1:13;
then (R_EAL (1 / (n + 1))) * (M . Br) = 0 by A10, A25, MESFUNC6:97;
then M . Br = 0 ;
hence ex B being Element of S st S₁[n,B] by A15, XBOOLE_1:28; :: thesis: verum

end;

consider F being Function of NAT ,S such that
A29: for n being Element of NAT holds S₁[n,F . n] from FUNCT_2:sch 3(A8);

now

let y be set ; :: thesis: ( y in { x where x is Element of X : ( x in dom f & f . x <> 0 ) } implies y in union (rng F) )
assume y in { x where x is Element of X : ( x in dom f & f . x <> 0 ) } ; :: thesis: y in union (rng F)
then consider z being Element of X such that
A32: ( y = z & z in dom f & f . z <> 0 ) ;
A33: z in dom (abs f) by A32, VALUED_1:def 11;
then (abs f) . z = abs (f . z) by VALUED_1:def 11;
then 0 < (abs f) . z by A32, COMPLEX1:133;
then consider n being Element of NAT such that
A34: 1 / (n + 1) < ((abs f) . z) - 0 by MESFUNC1:13;
z in great_eq_dom (abs f),(1 / (n + 1)) by A33, A34, MESFUNC6:6;
then A35: y in F . n by A29, A32;
F . n in rng F by FUNCT_2:6;
hence y in union (rng F) by A35, TARSKI:def 4; :: thesis: verum

end;

then A31: { x where x is Element of X : ( x in dom f & f . x <> 0 ) } c= union (rng F) by TARSKI:def 3;

now

let y be set ; :: thesis: ( y in union (rng F) implies y in { x where x is Element of X : ( x in dom f & f . x <> 0 ) } )
assume y in union (rng F) ; :: thesis: y in { x where x is Element of X : ( x in dom f & f . x <> 0 ) }
then consider B being set such that
A38: ( y in B & B in rng F ) by TARSKI:def 4;
consider n being set such that
A39: ( n in NAT & B = F . n ) by A38, FUNCT_2:17;
reconsider m = n as Element of NAT by A39;
A40: y in great_eq_dom (abs f),(1 / (m + 1)) by A29, A38, A39;
then A41: y in dom (abs f) by MESFUNC6:6;
then A46: y in dom f by VALUED_1:def 11;
A43: (abs f) . y <> 0 by A40, MESFUNC1:def 15;
(abs f) . y = abs (f . y) by A41, VALUED_1:def 11;
then f . y <> 0 by A43, ABSVALUE:7;
hence y in { x where x is Element of X : ( x in dom f & f . x <> 0 ) } by A46; :: thesis: verum

end;

then union (rng F) c= { x where x is Element of X : ( x in dom f & f . x <> 0 ) } by TARSKI:def 3;
then A30: { x where x is Element of X : ( x in dom f & f . x <> 0 ) } = union (rng F) by A31, XBOOLE_0:def 10;

now

let A be set ; :: thesis: ( A in rng F implies A is measure_zero of M )
assume A in rng F ; :: thesis: A is measure_zero of M
then consider n being set such that
A47: ( n in NAT & A = F . n ) by FUNCT_2:17;
reconsider n = n as Element of NAT by A47;
M . (F . n) = 0 by A29;
hence A is measure_zero of M by A47, MEASURE1:def 13; :: thesis: verum

end;

then A48: union (rng F) is measure_zero of M by MEASURE2:16;
reconsider EQ = (union (rng F)) \/ ND as Element of S ;
ND is measure_zero of M by A3, MEASURE1:def 13;
then EQ is measure_zero of M by A48, MEASURE1:70;
then A49: M . EQ = 0 by MEASURE1:def 13;
set g = X --> 0 ;
A51: EQ ` = (ND ` ) /\ ((union (rng F)) ` ) by XBOOLE_1:53;
then A51a: EQ ` c= dom f by A2, A3, XBOOLE_1:17;
A52: dom (f | (EQ ` )) = EQ ` by A2, A3, A51, RELAT_1:91, XBOOLE_1:17;
dom (X --> 0 ) = X by FUNCOP_1:19;
then A53: dom ((X --> 0 ) | (EQ ` )) = EQ ` by RELAT_1:91;

A54: now

let x be set ; :: thesis: ( x in EQ ` implies f . x = 0 )
assume A55: x in EQ ` ; :: thesis: f . x = 0
then x in (union (rng F)) ` by A51, XBOOLE_0:def 4;
then not x in union (rng F) by XBOOLE_0:def 5;
hence f . x = 0 by A30, A51a, A55; :: thesis: verum

end;

now

let y be set ; :: thesis: ( y in dom (f | (EQ ` )) implies (f | (EQ ` )) . y = ((X --> 0 ) | (EQ ` )) . y )
assume A57: y in dom (f | (EQ ` )) ; :: thesis: (f | (EQ ` )) . y = ((X --> 0 ) | (EQ ` )) . y
then (f | (EQ ` )) . y = f . y by FUNCT_1:70;
then (f | (EQ ` )) . y = 0 by A52, A54, A57;
then (f | (EQ ` )) . y = (X --> 0 ) . y by A57, FUNCOP_1:13;
hence (f | (EQ ` )) . y = ((X --> 0 ) | (EQ ` )) . y by A52, A53, A57, FUNCT_1:70; :: thesis: verum

end;

then f | (EQ ` ) = (X --> 0 ) | (EQ ` ) by A51a, A53, FUNCT_1:9, RELAT_1:91;
hence f a.e.= X --> 0 ,M by Def2, A49; :: thesis: verum