let I, J, K be non empty closed_interval Subset of REAL; :: thesis: for f being PartFunc of [:[:RNS_Real,RNS_Real:],RNS_Real:],RNS_Real
for g being PartFunc of [:[:REAL,REAL:],REAL:],REAL
for E being Element of sigma (measurable_rectangles ((sigma (measurable_rectangles (L-Field,L-Field))),L-Field)) st [:[:I,J:],K:] = dom f & f is_continuous_on [:[:I,J:],K:] & f = g & E = [:[:I,J:],K:] holds
g is E -measurable
let f be PartFunc of [:[:RNS_Real,RNS_Real:],RNS_Real:],RNS_Real; :: thesis: for g being PartFunc of [:[:REAL,REAL:],REAL:],REAL
for E being Element of sigma (measurable_rectangles ((sigma (measurable_rectangles (L-Field,L-Field))),L-Field)) st [:[:I,J:],K:] = dom f & f is_continuous_on [:[:I,J:],K:] & f = g & E = [:[:I,J:],K:] holds
g is E -measurable
let g be PartFunc of [:[:REAL,REAL:],REAL:],REAL; :: thesis: for E being Element of sigma (measurable_rectangles ((sigma (measurable_rectangles (L-Field,L-Field))),L-Field)) st [:[:I,J:],K:] = dom f & f is_continuous_on [:[:I,J:],K:] & f = g & E = [:[:I,J:],K:] holds
g is E -measurable
let E be Element of sigma (measurable_rectangles ((sigma (measurable_rectangles (L-Field,L-Field))),L-Field)); :: thesis: ( [:[:I,J:],K:] = dom f & f is_continuous_on [:[:I,J:],K:] & f = g & E = [:[:I,J:],K:] implies g is E -measurable )
assume that
A1: [:[:I,J:],K:] = dom f and
A2: f is_continuous_on [:[:I,J:],K:] and
A3: f = g and
A4: E = [:[:I,J:],K:] ; :: thesis: g is E -measurable
for r being Real holds E /\ (less_dom (g,r)) in sigma (measurable_rectangles ((sigma (measurable_rectangles (L-Field,L-Field))),L-Field))

proof

let r be Real; :: thesis: E /\ (less_dom (g,r)) in sigma (measurable_rectangles ((sigma (measurable_rectangles (L-Field,L-Field))),L-Field))
A5: less_dom (g,r) = g " ].-infty,r.[ by MESFUN16:17;
consider H being Subset of [:RNS_Real,RNS_Real,RNS_Real:] such that
A6: ( H /\ E = f " ].-infty,r.[ & H is open ) by A1, A2, A4, MESFUN16:24;
H in sigma (measurable_rectangles ((sigma (measurable_rectangles (L-Field,L-Field))),L-Field)) by A6, Th7;
then f " ].-infty,r.[ in sigma (measurable_rectangles ((sigma (measurable_rectangles (L-Field,L-Field))),L-Field)) by A6, FINSUB_1:def 2;
hence E /\ (less_dom (g,r)) in sigma (measurable_rectangles ((sigma (measurable_rectangles (L-Field,L-Field))),L-Field)) by A3, A5, FINSUB_1:def 2; :: thesis: verum

end;

hence g is E -measurable by MESFUNC6:12; :: thesis: verum