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
for E being Element of S st E = dom f & f is nonnegative & f is E -measurable & Integral (M,f) = 0 holds
f a.e.= (X --> 0) | E,M
let S be SigmaField of X; :: thesis: for M being sigma_Measure of S
for f being PartFunc of X,REAL
for E being Element of S st E = dom f & f is nonnegative & f is E -measurable & Integral (M,f) = 0 holds
f a.e.= (X --> 0) | E,M
let M be sigma_Measure of S; :: thesis: for f being PartFunc of X,REAL
for E being Element of S st E = dom f & f is nonnegative & f is E -measurable & Integral (M,f) = 0 holds
f a.e.= (X --> 0) | E,M
let f be PartFunc of X,REAL; :: thesis: for E being Element of S st E = dom f & f is nonnegative & f is E -measurable & Integral (M,f) = 0 holds
f a.e.= (X --> 0) | E,M
let E be Element of S; :: thesis: ( E = dom f & f is nonnegative & f is E -measurable & Integral (M,f) = 0 implies f a.e.= (X --> 0) | E,M )
assume that
A1: E = dom f and
A2: f is nonnegative and
A3: f is E -measurable and
A4: Integral (M,f) = 0 ; :: thesis: f a.e.= (X --> 0) | E,M
A5: ( E = dom (R_EAL f) & R_EAL f is nonnegative & R_EAL f is E -measurable & Integral (M,(R_EAL f)) = 0 ) by A1, A2, A3, A4, MESFUNC5:def 7, MESFUNC6:def 1, MESFUNC6:def 3;
then A6: M . (E /\ (great_dom ((R_EAL f),0))) = 0 by Th24;
reconsider A = E /\ (great_dom ((R_EAL f),0)) as Element of S by A5, MESFUNC1:29;
A7: (X --> 0) | E = (X /\ E) --> 0 by FUNCOP_1:12
.= E --> 0 by XBOOLE_1:28 ;
then A8: ( dom (f | (A `)) = (dom f) /\ (A `) & dom (((X --> 0) | E) | (A `)) = (dom (E --> 0)) /\ (A `) ) by RELAT_1:61;

now :: thesis: for x being Element of X st x in dom (f | (A `)) holds
(f | (A `)) . x = (((X --> 0) | E) | (A `)) . x

let x be Element of X; :: thesis: ( x in dom (f | (A `)) implies (f | (A `)) . x = (((X --> 0) | E) | (A `)) . x )
assume A9: x in dom (f | (A `)) ; :: thesis: (f | (A `)) . x = (((X --> 0) | E) | (A `)) . x
then A10: ( x in dom f & x in A ` ) by RELAT_1:57;
then x in X \ A by SUBSET_1:def 4;
then not x in A by XBOOLE_0:def 5;
then ( not x in E or not x in great_dom ((R_EAL f),0) ) by XBOOLE_0:def 4;
then A11: ( not x in dom (R_EAL f) or (R_EAL f) . x <= 0 ) by A9, A1, RELAT_1:57, MESFUNC1:def 13;
(R_EAL f) . x >= 0 by A5, SUPINF_2:51;
then f . x = 0 by A10, A11, MESFUNC5:def 7;
then A12: (f | (A `)) . x = 0 by A9, FUNCT_1:47;
A13: x in E /\ (A `) by A10, A1, XBOOLE_0:def 4;
(((X --> 0) | E) | (A `)) . x = ((E /\ (A `)) --> 0) . x by A7, FUNCOP_1:12;
hence (f | (A `)) . x = (((X --> 0) | E) | (A `)) . x by A12, A13, FUNCOP_1:7; :: thesis: verum

end;

hence f a.e.= (X --> 0) | E,M by A1, A6, A8, PARTFUN1:5, LPSPACE1:def 10; :: thesis: verum