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;

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

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