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 is nonnegative & R_EAL f is E -measurable & Integral (M,()) = 0 ) by ;
then A6: M . (E /\ (great_dom ((),0))) = 0 by Th24;
reconsider A = E /\ (great_dom ((),0)) as Element of S by ;
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 ((),0) ) by XBOOLE_0:def 4;
then A11: ( not x in dom () or () . x <= 0 ) by ;
(R_EAL f) . x >= 0 by ;
then f . x = 0 by ;
then A12: (f | (A `)) . x = 0 by ;
A13: x in E /\ (A `) by ;
(((X --> 0) | E) | (A `)) . x = ((E /\ (A `)) --> 0) . x by ;
hence (f | (A `)) . x = (((X --> 0) | E) | (A `)) . x by ; :: thesis: verum
end;
hence f a.e.= (X --> 0) | E,M by ; :: thesis: verum