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 A3, LPSPACE1:def 10;
set E2 = dom g;
( E ` = X \ E & X in S ) by SUBSET_1:def 4, MEASURE1:7;
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 A4, XBOOLE_1:17;
then A7: A c= dom (R_EAL f) by MESFUNC5:def 7;
dom (f | (E `)) = A by A4, RELAT_1:61;
then A8: A c= dom (R_EAL (g | (E `))) by A5, MESFUNC5:def 7;
A9: (R_EAL f) | A = f | A by MESFUNC5:def 7
.= (f | (E `)) | A by XBOOLE_1:17, RELAT_1:74
.= g | A by A5, XBOOLE_1:17, RELAT_1:74
.= R_EAL (g | A) by MESFUNC5:def 7 ;
g | A = (g | (E `)) | A by XBOOLE_1:17, RELAT_1:74;
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
.= (R_EAL g) | (E `) by MESFUNC5:def 7 ;
A c= E1 by XBOOLE_1:17;
then R_EAL f is A -measurable by A2, MESFUNC6:def 1, MESFUNC1:30;
then R_EAL (g | (E `)) is A -measurable by A7, A8, A9, A10, MESFUN12:36;
then A12: R_EAL g is A -measurable by A11, A6, XBOOLE_1:17, MESFUN13:19;
for r being Real holds E1 /\ (less_dom ((R_EAL g),r)) in S

proof

let r be Real; :: thesis: E1 /\ (less_dom ((R_EAL g),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 A5, MEASURE1:8, XBOOLE_1:17;
then M . (E1 /\ E) = 0 by SUPINF_2:51;
then A14: (E1 \ A) /\ (less_dom ((R_EAL g),r)) in S by A13, A1, XBOOLE_1:17, MEASURE3:def 1;
A15: A /\ (less_dom ((R_EAL g),r)) in S by A12, MESFUNC1:def 16;
((E1 \ A) /\ (less_dom ((R_EAL g),r))) \/ (A /\ (less_dom ((R_EAL g),r))) = ((E1 \ A) \/ A) /\ (less_dom ((R_EAL g),r)) by XBOOLE_1:23
.= (E1 \/ A) /\ (less_dom ((R_EAL g),r)) by XBOOLE_1:39
.= E1 /\ (less_dom ((R_EAL g),r)) by XBOOLE_1:12, XBOOLE_1:17 ;
hence E1 /\ (less_dom ((R_EAL g),r)) in S by A14, A15, FINSUB_1:def 1; :: thesis: verum

end;

hence g is E1 -measurable by MESFUNC1:def 16, MESFUNC6:def 1; :: thesis: verum