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 RF = Integral2 (L-Meas,(R_EAL g));
set IJ = [: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:] ;
A6: dom (Integral2 (L-Meas,(R_EAL g))) = [:REAL,REAL:] by FUNCT_2:def 1;
set F0 = (Integral2 (L-Meas,|.(R_EAL g).|)) | [:I,J:];
set RF0 = (Integral2 (L-Meas,(R_EAL g))) | [:I,J:];
reconsider K0 = K as Element of L-Field by MEASUR10:5, MEASUR12:75;
reconsider G = (Integral2 (L-Meas,|.(R_EAL g).|)) | [:I,J:] as PartFunc of [:REAL,REAL:],REAL by A1, A2, A3, Th32;
reconsider RG = (Integral2 (L-Meas,(R_EAL g))) | [:I,J:] as PartFunc of [:REAL,REAL:],REAL by A1, A2, A3, Th32;
( I in L-Field & J in L-Field ) by MEASUR10:5, MEASUR12:75;
then A7: [:I,J:] in measurable_rectangles (L-Field,L-Field) ;
measurable_rectangles (L-Field,L-Field) c= sigma (measurable_rectangles (L-Field,L-Field)) by PROB_1:def 9;
then reconsider AB = [:I,J:] as Element of sigma (measurable_rectangles (L-Field,L-Field)) by A7;
reconsider GG = G as PartFunc of [:RNS_Real,RNS_Real:],RNS_Real ;
reconsider RGG = RG 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 A8: (Integral2 (L-Meas,|.(R_EAL g).|)) | [:I,J:] is_integrable_on Prod_Measure (L-Meas,L-Meas) by MESFUNC5:def 7;
RGG is_uniformly_continuous_on [:I,J:] by A1, A2, A3, Th34;
then A9: RGG is_continuous_on [:I,J:] by NFCONT_2:7;
reconsider RG1 = (Integral2 (L-Meas,(R_EAL RG))) | I as PartFunc of REAL,REAL by A6, A9, MESFUN16:51;
[:REAL,REAL:] in sigma (measurable_rectangles (L-Field,L-Field)) by PROB_1:5;
then reconsider NAB = [:REAL,REAL:] \ AB as Element of sigma (measurable_rectangles (L-Field,L-Field)) by PROB_1:6;
A10: AB \/ NAB = [:REAL,REAL:] by XBOOLE_1:45;
A11: Integral2 (L-Meas,|.(R_EAL g).|) is nonnegative by A1, A2, A3, Th38;
reconsider H = [:REAL,REAL:] as Element of sigma (measurable_rectangles (L-Field,L-Field)) by PROB_1:5;
for r being Real holds H /\ (less_dom ((Integral2 (L-Meas,|.(R_EAL g).|)),r)) in sigma (measurable_rectangles (L-Field,L-Field))

proof

let r be Real; :: thesis: H /\ (less_dom ((Integral2 (L-Meas,|.(R_EAL g).|)),r)) in sigma (measurable_rectangles (L-Field,L-Field))
consider H0 being Element of sigma (measurable_rectangles (L-Field,L-Field)) such that
A12: ( H0 = dom ((Integral2 (L-Meas,|.(R_EAL g).|)) | [:I,J:]) & (Integral2 (L-Meas,|.(R_EAL g).|)) | [:I,J:] is H0 -measurable ) by A8, MESFUNC5:def 17;

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

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

now :: thesis: not less_dom ((Integral2 (L-Meas,|.(R_EAL g).|)),r) <> {}

assume less_dom ((Integral2 (L-Meas,|.(R_EAL g).|)),r) <> {} ; :: thesis: contradiction
then consider x being object such that
A14: 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 MESFUNC1:def 11, A14;
hence contradiction by A11, A13; :: thesis: verum

end;

hence H /\ (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 A15: 0 < r ; :: thesis: H /\ (less_dom ((Integral2 (L-Meas,|.(R_EAL g).|)),r)) in sigma (measurable_rectangles (L-Field,L-Field))

A16: H0 /\ (less_dom (((Integral2 (L-Meas,|.(R_EAL g).|)) | [:I,J:]),r)) in sigma (measurable_rectangles (L-Field,L-Field)) by A12;
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)) \/ NAB )

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)) \/ NAB )

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

assume A17: 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)) \/ NAB
then A18: ( z in dom (Integral2 (L-Meas,|.(R_EAL g).|)) & (Integral2 (L-Meas,|.(R_EAL g).|)) . z < r ) by MESFUNC1:def 11;

per cases ( z in AB or z in NAB ) by A17, A10, XBOOLE_0:def 3;

suppose A19: z in AB ; :: thesis: z in (less_dom (((Integral2 (L-Meas,|.(R_EAL g).|)) | [:I,J:]),r)) \/ NAB

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

end;

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

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

end;

end;

end;

assume z in (less_dom (((Integral2 (L-Meas,|.(R_EAL g).|)) | [:I,J:]),r)) \/ NAB ; :: 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 NAB ) by XBOOLE_0:def 3;

suppose A20: 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 A21: ( 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;
A22: (Integral2 (L-Meas,|.(R_EAL g).|)) . z < r by A4, A21, FUNCT_1:49;
dom (Integral2 (L-Meas,|.(R_EAL g).|)) = [:REAL,REAL:] by FUNCT_2:def 1;
hence z in less_dom ((Integral2 (L-Meas,|.(R_EAL g).|)),r) by A20, A22, MESFUNC1:def 11; :: thesis: verum

end;

suppose A23: z in NAB ; :: thesis: z in less_dom ((Integral2 (L-Meas,|.(R_EAL g).|)),r)

then reconsider x = z as Element of [:REAL,REAL:] ;
not z in AB by A23, XBOOLE_0:def 5;
then A24: (Integral2 (L-Meas,|.(R_EAL g).|)) . x < r by A15, A1, A3, Lm4;
dom (Integral2 (L-Meas,|.(R_EAL g).|)) = [:REAL,REAL:] by FUNCT_2:def 1;
hence z in less_dom ((Integral2 (L-Meas,|.(R_EAL g).|)),r) by A24, 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)) \/ NAB by TARSKI:2;
then A25: H /\ (less_dom ((Integral2 (L-Meas,|.(R_EAL g).|)),r)) = (AB /\ ((less_dom (((Integral2 (L-Meas,|.(R_EAL g).|)) | [:I,J:]),r)) \/ NAB)) \/ (NAB /\ ((less_dom (((Integral2 (L-Meas,|.(R_EAL g).|)) | [:I,J:]),r)) \/ NAB)) by A10, XBOOLE_1:23;
A26: AB /\ ((less_dom (((Integral2 (L-Meas,|.(R_EAL g).|)) | [:I,J:]),r)) \/ NAB) = AB /\ (less_dom (((Integral2 (L-Meas,|.(R_EAL g).|)) | [:I,J:]),r)) by XBOOLE_1:78, XBOOLE_1:85;
less_dom (((Integral2 (L-Meas,|.(R_EAL g).|)) | [:I,J:]),r) c= AB by A5, MESFUNC1:def 11;
then NAB misses less_dom (((Integral2 (L-Meas,|.(R_EAL g).|)) | [:I,J:]),r) ;
then NAB /\ ((less_dom (((Integral2 (L-Meas,|.(R_EAL g).|)) | [:I,J:]),r)) \/ NAB) = NAB /\ NAB by XBOOLE_1:78;
hence H /\ (less_dom ((Integral2 (L-Meas,|.(R_EAL g).|)),r)) in sigma (measurable_rectangles (L-Field,L-Field)) by A16, A4, A12, A25, A26, PROB_1:3; :: thesis: verum

end;

end;

end;

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