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

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

hence
g is E1 -measurable
by MESFUNC1:def 16, MESFUNC6:def 1; :: thesis: verum
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;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