let n be non zero Nat; :: thesis: for I being Subset of (CarProduct ((Seg n) --> REAL))
for J being Subset of REAL
for f being PartFunc of [:(CarProduct ((Seg n) --> RNS_Real)),RNS_Real:],RNS_Real
for g being PartFunc of [:(CarProduct ((Seg n) --> REAL)),REAL:],REAL
for E being Element of sigma (measurable_rectangles ((Prod_Field (L-Field n)),L-Field)) st [:I,J:] = dom f & f is_continuous_on [:I,J:] & f = g & E = [:I,J:] holds
g is E -measurable
let I be Subset of (CarProduct ((Seg n) --> REAL)); :: thesis: for J being Subset of REAL
for f being PartFunc of [:(CarProduct ((Seg n) --> RNS_Real)),RNS_Real:],RNS_Real
for g being PartFunc of [:(CarProduct ((Seg n) --> REAL)),REAL:],REAL
for E being Element of sigma (measurable_rectangles ((Prod_Field (L-Field n)),L-Field)) st [:I,J:] = dom f & f is_continuous_on [:I,J:] & f = g & E = [:I,J:] holds
g is E -measurable
let J be Subset of REAL; :: thesis: for f being PartFunc of [:(CarProduct ((Seg n) --> RNS_Real)),RNS_Real:],RNS_Real
for g being PartFunc of [:(CarProduct ((Seg n) --> REAL)),REAL:],REAL
for E being Element of sigma (measurable_rectangles ((Prod_Field (L-Field n)),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 [:(CarProduct ((Seg n) --> RNS_Real)),RNS_Real:],RNS_Real; :: thesis: for g being PartFunc of [:(CarProduct ((Seg n) --> REAL)),REAL:],REAL
for E being Element of sigma (measurable_rectangles ((Prod_Field (L-Field n)),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 [:(CarProduct ((Seg n) --> REAL)),REAL:],REAL; :: thesis: for E being Element of sigma (measurable_rectangles ((Prod_Field (L-Field n)),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 ((Prod_Field (L-Field n)),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 ((Prod_Field (L-Field n)),L-Field))

proof

let r be Real; :: thesis: E /\ (less_dom (g,r)) in sigma (measurable_rectangles ((Prod_Field (L-Field n)),L-Field))
A5: less_dom (g,r) = g " ].-infty,r.[ by MESFUN16:17;
consider H being Subset of [:(CarProduct ((Seg n) --> RNS_Real)),RNS_Real:] such that
A6: ( H /\ E = f " ].-infty,r.[ & H is open ) by A1, A2, A4, MESFUN16:24;
CarProduct ((Seg (n + 1)) --> RNS_Real) = [:(CarProduct ((Seg n) --> RNS_Real)),RNS_Real:] by MEASUR15:38;
then A7: H in Prod_Field (L-Field (n + 1)) by A6, MEASUR15:65;
Prod_Field (L-Field (n + 1)) = sigma (measurable_rectangles ((Prod_Field (L-Field n)),L-Field)) by MEASUR14:44;
then f " ].-infty,r.[ in sigma (measurable_rectangles ((Prod_Field (L-Field n)),L-Field)) by A6, A7, FINSUB_1:def 2;
hence E /\ (less_dom (g,r)) in sigma (measurable_rectangles ((Prod_Field (L-Field n)),L-Field)) by A3, A5, FINSUB_1:def 2; :: thesis: verum

end;

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