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 (L-Field,L-Field)) st [:[:I,J:],K:] = dom f & f is_continuous_on [:[:I,J:],K:] & f = g holds
Integral2 (L-Meas,|.(R_EAL 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 (L-Field,L-Field)) st [:[:I,J:],K:] = dom f & f is_continuous_on [:[:I,J:],K:] & f = g holds
Integral2 (L-Meas,|.(R_EAL g).|) is E -measurable
let g be PartFunc of [:[:REAL,REAL:],REAL:],REAL; :: thesis: for E being Element of sigma (measurable_rectangles (L-Field,L-Field)) st [:[:I,J:],K:] = dom f & f is_continuous_on [:[:I,J:],K:] & f = g holds
Integral2 (L-Meas,|.(R_EAL g).|) is E -measurable
let E be Element of sigma (measurable_rectangles (L-Field,L-Field)); :: thesis: ( [:[:I,J:],K:] = dom f & f is_continuous_on [:[:I,J:],K:] & f = g implies Integral2 (L-Meas,|.(R_EAL 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 ; :: thesis: Integral2 (L-Meas,|.(R_EAL g).|) is E -measurable
set F = Integral2 (L-Meas,|.(R_EAL g).|);
set F0 = (Integral2 (L-Meas,|.(R_EAL g).|)) | [:I,J:];
A4: dom (Integral2 (L-Meas,|.(R_EAL g).|)) = [:REAL,REAL:] by FUNCT_2:def 1;
then A5: dom ((Integral2 (L-Meas,|.(R_EAL g).|)) | [:I,J:]) = [:I,J:] ;
reconsider G = (Integral2 (L-Meas,|.(R_EAL g).|)) | [:I,J:] as PartFunc of [:REAL,REAL:],REAL by A1, A2, A3, Th32;
reconsider GG = G as PartFunc of [:RNS_Real,RNS_Real:],RNS_Real ;
GG is_uniformly_continuous_on [:I,J:] by A1, A2, A3, Th33;
then GG is_continuous_on [:I,J:] by NFCONT_2:7;
then G is_integrable_on Prod_Measure (L-Meas,L-Meas) by A4, MESFUN16:57;
then A6: (Integral2 (L-Meas,|.(R_EAL g).|)) | [:I,J:] is_integrable_on Prod_Measure (L-Meas,L-Meas) by MESFUNC5:def 7;
reconsider IJ = [:I,J:] as Element of sigma (measurable_rectangles (L-Field,L-Field)) by MESFUN16:11;
reconsider R2 = [:REAL,REAL:] as Element of sigma (measurable_rectangles (L-Field,L-Field)) by PROB_1:5;
set NIJ = R2 \ IJ;
A7: IJ \/ (R2 \ IJ) = [:REAL,REAL:] by XBOOLE_1:45;
A8: IJ /\ (R2 \ IJ) = {} by XBOOLE_1:85, XBOOLE_0:def 7;
A9: Integral2 (L-Meas,|.(R_EAL g).|) is nonnegative by A1, A2, A3, Th38;
for r being Real holds R2 /\ (less_dom ((Integral2 (L-Meas,|.(R_EAL g).|)),r)) in sigma (measurable_rectangles (L-Field,L-Field))

proof

let r be Real; :: thesis: R2 /\ (less_dom ((Integral2 (L-Meas,|.(R_EAL g).|)),r)) in sigma (measurable_rectangles (L-Field,L-Field))
A10: ex E being Element of sigma (measurable_rectangles (L-Field,L-Field)) st
( E = dom ((Integral2 (L-Meas,|.(R_EAL g).|)) | [:I,J:]) & (Integral2 (L-Meas,|.(R_EAL g).|)) | [:I,J:] is E -measurable ) by A6, MESFUNC5:def 17;

per cases ( r <= 0 or 0 < r ) ;

suppose A11: r <= 0 ; :: thesis: R2 /\ (less_dom ((Integral2 (L-Meas,|.(R_EAL g).|)),r)) in sigma (measurable_rectangles (L-Field,L-Field))

less_dom ((Integral2 (L-Meas,|.(R_EAL g).|)),r) = {}

proof

assume less_dom ((Integral2 (L-Meas,|.(R_EAL g).|)),r) <> {} ; :: thesis: contradiction
then consider x being object such that
A12: x in less_dom ((Integral2 (L-Meas,|.(R_EAL g).|)),r) by XBOOLE_0:def 1;
( x in dom (Integral2 (L-Meas,|.(R_EAL g).|)) & (Integral2 (L-Meas,|.(R_EAL g).|)) . x < r ) by A12, MESFUNC1:def 11;
hence contradiction by A9, A11; :: thesis: verum

end;

hence R2 /\ (less_dom ((Integral2 (L-Meas,|.(R_EAL g).|)),r)) in sigma (measurable_rectangles (L-Field,L-Field)) by PROB_1:4; :: thesis: verum

end;

suppose A13: 0 < r ; :: thesis: R2 /\ (less_dom ((Integral2 (L-Meas,|.(R_EAL g).|)),r)) in sigma (measurable_rectangles (L-Field,L-Field))

for z being object holds
( z in less_dom ((Integral2 (L-Meas,|.(R_EAL g).|)),r) iff z in (less_dom (((Integral2 (L-Meas,|.(R_EAL g).|)) | [:I,J:]),r)) \/ (R2 \ IJ) )

proof

let z be object ; :: thesis: ( z in less_dom ((Integral2 (L-Meas,|.(R_EAL g).|)),r) iff z in (less_dom (((Integral2 (L-Meas,|.(R_EAL g).|)) | [:I,J:]),r)) \/ (R2 \ IJ) )

hereby :: thesis: ( z in (less_dom (((Integral2 (L-Meas,|.(R_EAL g).|)) | [:I,J:]),r)) \/ (R2 \ IJ) implies z in less_dom ((Integral2 (L-Meas,|.(R_EAL g).|)),r) )

assume A14: z in less_dom ((Integral2 (L-Meas,|.(R_EAL g).|)),r) ; :: thesis: z in (less_dom (((Integral2 (L-Meas,|.(R_EAL g).|)) | [:I,J:]),r)) \/ (R2 \ IJ)
then A15: (Integral2 (L-Meas,|.(R_EAL g).|)) . z < r by MESFUNC1:def 11;
A16: ( z in R2 \ IJ implies z in (less_dom (((Integral2 (L-Meas,|.(R_EAL g).|)) | [:I,J:]),r)) \/ (R2 \ IJ) ) by XBOOLE_0:def 3;

now :: thesis: ( z in IJ implies z in (less_dom (((Integral2 (L-Meas,|.(R_EAL g).|)) | [:I,J:]),r)) \/ (R2 \ IJ) )

assume A17: z in IJ ; :: thesis: z in (less_dom (((Integral2 (L-Meas,|.(R_EAL g).|)) | [:I,J:]),r)) \/ (R2 \ IJ)
then ((Integral2 (L-Meas,|.(R_EAL g).|)) | [:I,J:]) . z < r by A15, FUNCT_1:49;
then z in less_dom (((Integral2 (L-Meas,|.(R_EAL g).|)) | [:I,J:]),r) by A5, A17, MESFUNC1:def 11;
hence z in (less_dom (((Integral2 (L-Meas,|.(R_EAL g).|)) | [:I,J:]),r)) \/ (R2 \ IJ) by XBOOLE_0:def 3; :: thesis: verum

end;

hence z in (less_dom (((Integral2 (L-Meas,|.(R_EAL g).|)) | [:I,J:]),r)) \/ (R2 \ IJ) by A7, A14, A16, XBOOLE_0:def 3; :: thesis: verum

end;

assume z in (less_dom (((Integral2 (L-Meas,|.(R_EAL g).|)) | [:I,J:]),r)) \/ (R2 \ IJ) ; :: thesis: z in less_dom ((Integral2 (L-Meas,|.(R_EAL g).|)),r)

per cases then ( z in less_dom (((Integral2 (L-Meas,|.(R_EAL g).|)) | [:I,J:]),r) or z in R2 \ IJ ) by XBOOLE_0:def 3;

suppose A18: z in less_dom (((Integral2 (L-Meas,|.(R_EAL g).|)) | [:I,J:]),r) ; :: thesis: z in less_dom ((Integral2 (L-Meas,|.(R_EAL g).|)),r)

then ( z in dom ((Integral2 (L-Meas,|.(R_EAL g).|)) | [:I,J:]) & ((Integral2 (L-Meas,|.(R_EAL g).|)) | [:I,J:]) . z < r ) by MESFUNC1:def 11;
then (Integral2 (L-Meas,|.(R_EAL g).|)) . z < r by A4, FUNCT_1:49;
hence z in less_dom ((Integral2 (L-Meas,|.(R_EAL g).|)),r) by A4, A18, MESFUNC1:def 11; :: thesis: verum

end;

suppose A19: z in R2 \ IJ ; :: thesis: z in less_dom ((Integral2 (L-Meas,|.(R_EAL g).|)),r)

then not z in IJ by XBOOLE_0:def 5;
then (Integral2 (L-Meas,|.(R_EAL g).|)) . z < r by A13, A1, A3, A19, Lm4;
hence z in less_dom ((Integral2 (L-Meas,|.(R_EAL g).|)),r) by A4, A19, MESFUNC1:def 11; :: thesis: verum

end;

end;

end;

then less_dom ((Integral2 (L-Meas,|.(R_EAL g).|)),r) = (less_dom (((Integral2 (L-Meas,|.(R_EAL g).|)) | [:I,J:]),r)) \/ (R2 \ IJ) by TARSKI:2;
then A20: R2 /\ (less_dom ((Integral2 (L-Meas,|.(R_EAL g).|)),r)) = (IJ /\ ((less_dom (((Integral2 (L-Meas,|.(R_EAL g).|)) | [:I,J:]),r)) \/ (R2 \ IJ))) \/ ((R2 \ IJ) /\ ((less_dom (((Integral2 (L-Meas,|.(R_EAL g).|)) | [:I,J:]),r)) \/ (R2 \ IJ))) by A7, XBOOLE_1:23;
IJ /\ ((less_dom (((Integral2 (L-Meas,|.(R_EAL g).|)) | [:I,J:]),r)) \/ (R2 \ IJ)) = (IJ /\ (less_dom (((Integral2 (L-Meas,|.(R_EAL g).|)) | [:I,J:]),r))) \/ (IJ /\ (R2 \ IJ)) by XBOOLE_1:23;
then A21: IJ /\ ((less_dom (((Integral2 (L-Meas,|.(R_EAL g).|)) | [:I,J:]),r)) \/ (R2 \ IJ)) in sigma (measurable_rectangles (L-Field,L-Field)) by A4, A8, A10;
A22: less_dom (((Integral2 (L-Meas,|.(R_EAL g).|)) | [:I,J:]),r) c= IJ by A5, MESFUNC1:def 11;
(R2 \ IJ) /\ ((less_dom (((Integral2 (L-Meas,|.(R_EAL g).|)) | [:I,J:]),r)) \/ (R2 \ IJ)) = ((R2 \ IJ) /\ (less_dom (((Integral2 (L-Meas,|.(R_EAL g).|)) | [:I,J:]),r))) \/ ((R2 \ IJ) /\ (R2 \ IJ)) by XBOOLE_1:23;
then (R2 \ IJ) /\ ((less_dom (((Integral2 (L-Meas,|.(R_EAL g).|)) | [:I,J:]),r)) \/ (R2 \ IJ)) = {} \/ ((R2 \ IJ) /\ (R2 \ IJ)) by A22;
hence R2 /\ (less_dom ((Integral2 (L-Meas,|.(R_EAL g).|)),r)) in sigma (measurable_rectangles (L-Field,L-Field)) by A20, A21, PROB_1:3; :: thesis: verum

end;

end;

end;

then Integral2 (L-Meas,|.(R_EAL g).|) is R2 -measurable ;
hence Integral2 (L-Meas,|.(R_EAL g).|) is E -measurable by MESFUNC1:30; :: thesis: verum