let X be non empty set ; :: thesis: for S being SigmaField of X
for M being sigma_Measure of S
for f, g being PartFunc of X,REAL
for E1 being Element of S st M is complete & f is E1 -measurable & f a.e.= g,M & E1 = dom f holds
g is E1 -measurable

let S be SigmaField of X; :: thesis: for M being sigma_Measure of S
for f, g being PartFunc of X,REAL
for E1 being Element of S st M is complete & f is E1 -measurable & f a.e.= g,M & E1 = dom f holds
g is E1 -measurable

let M be sigma_Measure of S; :: thesis: for f, g being PartFunc of X,REAL
for E1 being Element of S st M is complete & f is E1 -measurable & f a.e.= g,M & E1 = dom f holds
g is E1 -measurable

let f, g be PartFunc of X,REAL; :: thesis: for E1 being Element of S st M is complete & f is E1 -measurable & f a.e.= g,M & E1 = dom f holds
g is E1 -measurable

let E1 be Element of S; :: thesis: ( M is complete & f is E1 -measurable & f a.e.= g,M & E1 = dom f implies g is E1 -measurable )
assume that
A1: M is complete and
A2: f is E1 -measurable and
A3: f a.e.= g,M and
A4: E1 = dom f ; :: thesis: g is E1 -measurable
consider E being Element of S such that
A5: ( M . E = 0 & f | (E `) = g | (E `) ) by ;
set E2 = dom g;
( E ` = X \ E & X in S ) by ;
then A6: E ` in S by MEASURE1:6;
then reconsider A = E1 /\ (E `) as Element of S by FINSUB_1:def 2;
A c= dom f by ;
then A7: A c= dom () by MESFUNC5:def 7;
dom (f | (E `)) = A by ;
then A8: A c= dom (R_EAL (g | (E `))) by ;
A9: () | A = f | A by MESFUNC5:def 7
.= (f | (E `)) | A by
.= g | A by
.= R_EAL (g | A) by MESFUNC5:def 7 ;
g | A = (g | (E `)) | A by ;
then R_EAL (g | A) = (g | (E `)) | A by MESFUNC5:def 7;
then A10: R_EAL (g | A) = (R_EAL (g | (E `))) | A by MESFUNC5:def 7;
A11: R_EAL (g | (E `)) = g | (E `) by MESFUNC5:def 7
.= () | (E `) by MESFUNC5:def 7 ;
A c= E1 by XBOOLE_1:17;
then R_EAL f is A -measurable by ;
then R_EAL (g | (E `)) is A -measurable by ;
then A12: R_EAL g is A -measurable by ;
for r being Real holds E1 /\ (less_dom ((),r)) in S
proof
let r be Real; :: thesis: E1 /\ (less_dom ((),r)) in S
A13: E1 \ A = E1 \ (E `) by XBOOLE_1:47
.= E1 \ (X \ E) by SUBSET_1:def 4
.= (E1 \ X) \/ (E1 /\ E) by XBOOLE_1:52
.= {} \/ (E1 /\ E) by XBOOLE_1:37
.= E1 /\ E ;
M . (E1 /\ E) <= 0 by ;
then M . (E1 /\ E) = 0 by SUPINF_2:51;
then A14: (E1 \ A) /\ (less_dom ((),r)) in S by ;
A15: A /\ (less_dom ((),r)) in S by ;
((E1 \ A) /\ (less_dom ((),r))) \/ (A /\ (less_dom ((),r))) = ((E1 \ A) \/ A) /\ (less_dom ((),r)) by XBOOLE_1:23
.= (E1 \/ A) /\ (less_dom ((),r)) by XBOOLE_1:39
.= E1 /\ (less_dom ((),r)) by ;
hence E1 /\ (less_dom ((),r)) in S by ; :: thesis: verum
end;
hence g is E1 -measurable by ; :: thesis: verum