let I, J, K be non empty closed_interval Subset of REAL; :: thesis:
let f be PartFunc of [:[:RNS_Real,RNS_Real:],RNS_Real:],RNS_Real; :: thesis:
let g be PartFunc of [:[:REAL,REAL:],REAL:],REAL; :: thesis:
assume that
A1: [:[:I,J:],K:] = dom f and
A2: f is_continuous_on [:[:I,J:],K:] and
A3: f = g ; :: thesis:
set F = Integral2 (L-Meas,|.(R_EAL g).|);
set RF = Integral2 (L-Meas,(R_EAL g));
set IJ = [:I,J:];
A4: dom (R_EAL g) = dom f by A3, MESFUNC5:def 7;
A5: dom (Integral2 (L-Meas,|.(R_EAL g).|)) = [:REAL,REAL:] by FUNCT_2:def 1;
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 A5, MESFUN16:57;
then (Integral2 (L-Meas,|.(R_EAL g).|)) | [:I,J:] is_integrable_on Prod_Measure (L-Meas,L-Meas) by MESFUNC5:def 7;
then A8: Integral ((Prod_Measure (L-Meas,L-Meas)),((Integral2 (L-Meas,|.(R_EAL g).|)) | [:I,J:])) < +infty by MESFUNC5:96;
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;
A12: Integral2 (L-Meas,|.(R_EAL g).|) is H -measurable by A1, A2, A3, Th42;
set F1 = (Integral2 (L-Meas,|.(R_EAL g).|)) | NAB;
(Integral2 (L-Meas,|.(R_EAL g).|)) | (AB \/ NAB) = Integral2 (L-Meas,|.(R_EAL g).|) by A10;
then A13: Integral ((Prod_Measure (L-Meas,L-Meas)),(Integral2 (L-Meas,|.(R_EAL g).|))) = (Integral ((Prod_Measure (L-Meas,L-Meas)),((Integral2 (L-Meas,|.(R_EAL g).|)) | [:I,J:]))) + (Integral ((Prod_Measure (L-Meas,L-Meas)),((Integral2 (L-Meas,|.(R_EAL g).|)) | NAB))) by A5, A12, A11, MESFUNC5:91, XBOOLE_1:79;
for x being object st x in dom ((Integral2 (L-Meas,|.(R_EAL g).|)) | NAB) holds
((Integral2 (L-Meas,|.(R_EAL g).|)) | NAB) . x = 0

let x be object ; :: thesis:
assume A14: x in dom ((Integral2 (L-Meas,|.(R_EAL g).|)) | NAB) ; :: thesis:
then reconsider r = x as Element of [:REAL,REAL:] by A5;
not x in AB by A14, XBOOLE_0:def 5;
then (Integral2 (L-Meas,|.(R_EAL g).|)) . r = 0 by A1, A3, Lm4;
hence ((Integral2 (L-Meas,|.(R_EAL g).|)) | NAB) . x = 0 by FUNCT_1:49, A14; :: thesis:

end;

then Integral ((Prod_Measure (L-Meas,L-Meas)),((Integral2 (L-Meas,|.(R_EAL g).|)) | NAB)) = 0 * ((Prod_Measure (L-Meas,L-Meas)) . (dom ((Integral2 (L-Meas,|.(R_EAL g).|)) | NAB))) by A5, MEASUR10:27;
then A15: Integral ((Prod_Measure (L-Meas,L-Meas)),((Integral2 (L-Meas,|.(R_EAL g).|)) | [:I,J:])) = Integral ((Prod_Measure (L-Meas,L-Meas)),(Integral2 (L-Meas,|.(R_EAL g).|))) by A13, XXREAL_3:4;
reconsider KK = [:[:I,J:],K:] as Element of sigma (measurable_rectangles ((sigma (measurable_rectangles (L-Field,L-Field))),L-Field)) by Th4;
A16: g is KK -measurable by A1, A2, A3, Th29;
hence g is_integrable_on Prod_Measure ((Prod_Measure (L-Meas,L-Meas)),L-Meas) by A1, A4, A15, A8, MESFUN13:11, MESFUN16:5, MESFUN16:6; :: thesis:
A17: R_EAL g is_integrable_on Prod_Measure ((Prod_Measure (L-Meas,L-Meas)),L-Meas) by A16, MESFUN13:11, A1, A4, A15, A8, MESFUN16:5, MESFUN16:6;
for x being Element of [:REAL,REAL:] holds (Integral2 (L-Meas,|.(R_EAL g).|)) . x < +infty by A1, A2, A3, Th40;
hence ( ( for x being Element of [:REAL,REAL:] holds ProjPMap1 ((R_EAL g),x) is_integrable_on L-Meas ) & ( for U being Element of sigma (measurable_rectangles (L-Field,L-Field)) holds Integral2 (L-Meas,(R_EAL g)) is U -measurable ) & Integral2 (L-Meas,(R_EAL g)) is_integrable_on Prod_Measure (L-Meas,L-Meas) & Integral ((Prod_Measure ((Prod_Measure (L-Meas,L-Meas)),L-Meas)),g) = Integral ((Prod_Measure (L-Meas,L-Meas)),(Integral2 (L-Meas,(R_EAL g)))) ) by A17, MESFUN13:32, MESFUN16:5, MESFUN16:6; :: thesis: