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

proof

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

end;

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