let X be non empty set ; :: thesis:
let S be SigmaField of X; :: thesis:
let M be sigma_Measure of S; :: thesis:
let f be PartFunc of X,REAL; :: thesis:
assume that
A1: f in L1_Functions M and
A2: Integral (M,(abs f)) = 0 ; :: thesis:
set g = X --> 0;
defpred S₁[ Element of NAT , set ] means ( $2 = great_eq_dom ((abs f),(1 / ($1 + 1))) & M . $2 = 0 );
consider f1 being PartFunc of X,REAL such that
A3: f = f1 and
A4: ex ND being Element of S st
( M . ND = 0 & dom f1 = ND ` & f1 is_integrable_on M ) by A1;
A5: abs f is_integrable_on M by A3, A4, Th44;
then R_EAL (abs f) is_integrable_on M ;
then consider E being Element of S such that
A6: E = dom (R_EAL (abs f)) and
A7: R_EAL (abs f) is E -measurable ;
A8: abs f is E -measurable by A7;

let x be object ; :: thesis:
assume x in dom (abs f) ; :: thesis:
then (abs f) . x = |.(f . x).| by VALUED_1:def 11;
hence 0 <= (abs f) . x by COMPLEX1:46; :: thesis:

end;

then A9: abs f is nonnegative by MESFUNC6:52;

A10: now :: thesis:

let n be Element of NAT ; :: thesis:
reconsider r = 1 / (n + 1) as Element of REAL by XREAL_0:def 1;
reconsider Br = E /\ (great_eq_dom ((abs f),r)) as Element of S by A6, A8, MESFUNC6:13;
set g = Br --> r;
A11: dom (Br --> r) = Br by FUNCT_2:def 1;
A12: for x being set st x in dom (Br --> r) holds
(Br --> r) . x = r by FUNCOP_1:7;
reconsider g = Br --> r as PartFunc of X,REAL by RELSET_1:7;
A13: (abs f) | Br is_integrable_on M by A5, MESFUNC6:91;
for x being object st x in dom g holds
0 <= g . x by A12;
then g is nonnegative by MESFUNC6:52;
then A14: 0 <= Integral (M,g) by A11, A12, Th52, MESFUNC6:84;
A15: dom (abs g) = dom g by VALUED_1:def 11;

A16: now :: thesis:

let x be Element of X; :: thesis:
assume A17: x in dom (abs g) ; :: thesis:
then (abs g) . x = |.(g . x).| by VALUED_1:def 11;
then (abs g) . x = |.r.| by A12, A15, A17;
then (abs g) . x = r by ABSVALUE:def 1;
hence (abs g) . x = g . x by A12, A15, A17; :: thesis:

end;

A18: dom ((abs f) | Br) = (dom (abs f)) /\ Br by RELAT_1:61
.= Br by A6, XBOOLE_1:17, XBOOLE_1:28 ;
then A19: dom g = dom ((abs f) | Br) by FUNCT_2:def 1;

A20: now :: thesis:

let x be Element of X; :: thesis:
assume A21: x in dom g ; :: thesis:
then x in E /\ (great_eq_dom ((abs f),r)) by FUNCT_2:def 1;
then x in great_eq_dom ((abs f),r) by XBOOLE_0:def 4;
then A22: ex y being Real st
( y = (abs f) . x & r <= y ) by MESFUNC6:6;
|.(g . x).| = |.r.| by A12, A21;
then |.(g . x).| = r by ABSVALUE:def 1;
hence |.(g . x).| <= ((abs f) | Br) . x by A19, A21, A22, FUNCT_1:47; :: thesis:

end;

g is Br -measurable by A11, A12, Th52;
then Integral (M,(abs g)) <= Integral (M,((abs f) | Br)) by A11, A18, A13, A20, MESFUNC6:96;
then A23: Integral (M,g) <= Integral (M,((abs f) | Br)) by A15, A16, PARTFUN1:5;
A24: for x being object st x in dom g holds
g . x = r by A11, FUNCOP_1:7;
reconsider rr = r as R_eal ;
Integral (M,((abs f) | Br)) <= Integral (M,((abs f) | E)) by A6, A8, A9, MESFUNC6:87, XBOOLE_1:17;
then Integral (M,g) = 0 by A2, A6, A23, A14, RELAT_1:68;
then rr * (M . Br) = 0 by A11, A24, MESFUNC6:97;
then A25: M . Br = 0 ;
for x being object st x in great_eq_dom ((abs f),r) holds
x in dom (abs f) by MESFUNC6:6;
then great_eq_dom ((abs f),r) c= E by A6;
hence ex B being Element of S st S₁[n,B] by A25, XBOOLE_1:28; :: thesis:

end;

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

let y be object ; :: thesis:
assume y in union (rng F) ; :: thesis:
then consider B being set such that
A27: y in B and
A28: B in rng F by TARSKI:def 4;
consider n being object such that
A29: n in NAT and
A30: B = F . n by A28, FUNCT_2:11;
reconsider m = n as Element of NAT by A29;
A31: y in great_eq_dom ((abs f),(1 / (m + 1))) by A26, A27, A30;
then A32: y in dom (abs f) by MESFUNC6:6;
then A33: y in dom f by VALUED_1:def 11;
A34: (abs f) . y = |.(f . y).| by A32, VALUED_1:def 11;
(abs f) . y <> 0 by A31, MESFUNC1:def 14;
then f . y <> 0 by A34, ABSVALUE:2;
hence y in { x where x is Element of X : ( x in dom f & f . x <> 0 ) } by A33; :: thesis:

end;

then A35: union (rng F) c= { x where x is Element of X : ( x in dom f & f . x <> 0 ) } ;
consider ND being Element of S such that
A36: M . ND = 0 and
A37: dom f1 = ND ` and
f1 is_integrable_on M by A4;
reconsider EQ = (union (rng F)) \/ ND as Element of S ;
A38: EQ ` = (ND `) /\ ((union (rng F)) `) by XBOOLE_1:53;
then A39: EQ ` c= dom f by A3, A37, XBOOLE_1:17;
dom (X --> 0) = X by FUNCOP_1:13;
then A40: dom ((X --> 0) | (EQ `)) = EQ ` by RELAT_1:62;
A41: dom (f | (EQ `)) = EQ ` by A3, A37, A38, RELAT_1:62, XBOOLE_1:17;

let y be object ; :: thesis:
assume y in { x where x is Element of X : ( x in dom f & f . x <> 0 ) } ; :: thesis:
then consider z being Element of X such that
A42: y = z and
A43: z in dom f and
A44: f . z <> 0 ;
A45: z in dom (abs f) by A43, VALUED_1:def 11;
then (abs f) . z = |.(f . z).| by VALUED_1:def 11;
then 0 < (abs f) . z by A44, COMPLEX1:47;
then consider n being Element of NAT such that
A46: 1 / (n + 1) < ((abs f) . z) - 0 by MESFUNC1:10;
z in great_eq_dom ((abs f),(1 / (n + 1))) by A45, A46, MESFUNC6:6;
then A47: y in F . n by A26, A42;
F . n in rng F by FUNCT_2:4;
hence y in union (rng F) by A47, TARSKI:def 4; :: thesis:

end;

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

A49: now :: thesis:

let x be set ; :: thesis:
assume A50: x in EQ ` ; :: thesis:
then x in (union (rng F)) ` by A38, XBOOLE_0:def 4;
then not x in union (rng F) by XBOOLE_0:def 5;
hence f . x = 0 by A48, A39, A50; :: thesis:

end;

let y be object ; :: thesis:
assume A51: y in dom (f | (EQ `)) ; :: thesis:
then (f | (EQ `)) . y = f . y by FUNCT_1:47;
then (f | (EQ `)) . y = 0 by A41, A49, A51;
then (f | (EQ `)) . y = (X --> 0) . y by A51, FUNCOP_1:7;
hence (f | (EQ `)) . y = ((X --> 0) | (EQ `)) . y by A41, A40, A51, FUNCT_1:47; :: thesis:

end;

then A52: f | (EQ `) = (X --> 0) | (EQ `) by A39, A40, FUNCT_1:2, RELAT_1:62;

let A be set ; :: thesis:
assume A in rng F ; :: thesis:
then consider n being object such that
A53: n in NAT and
A54: A = F . n by FUNCT_2:11;
reconsider n = n as Element of NAT by A53;
M . (F . n) = 0 by A26;
hence A is measure_zero of M by A54, MEASURE1:def 7; :: thesis:

end;

then A55: union (rng F) is measure_zero of M by MEASURE2:14;
ND is measure_zero of M by A36, MEASURE1:def 7;
then EQ is measure_zero of M by A55, MEASURE1:37;
then M . EQ = 0 by MEASURE1:def 7;
hence f a.e.= X --> 0,M by A52; :: thesis: