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 st [:[:I,J:],K:] = dom f & f is_continuous_on [:[:I,J:],K:] & f = g holds
( ( for U being Element of L-Field holds Integral2 (L-Meas,(Integral2 (L-Meas,(R_EAL g)))) is U -measurable ) & Integral2 (L-Meas,(Integral2 (L-Meas,(R_EAL g)))) is_integrable_on L-Meas & Integral ((Prod_Measure (L-Meas,L-Meas)),(Integral2 (L-Meas,(R_EAL g)))) = Integral (L-Meas,(Integral2 (L-Meas,(Integral2 (L-Meas,(R_EAL g)))))) & Integral ((Prod_Measure ((Prod_Measure (L-Meas,L-Meas)),L-Meas)),g) = Integral (L-Meas,(Integral2 (L-Meas,(Integral2 (L-Meas,(R_EAL g)))))) & (Integral2 (L-Meas,(R_EAL g))) | [:I,J:] is_integrable_on Prod_Measure (L-Meas,L-Meas) & Integral ((Prod_Measure (L-Meas,L-Meas)),((Integral2 (L-Meas,(R_EAL g))) | [:I,J:])) = Integral (L-Meas,(Integral2 (L-Meas,((Integral2 (L-Meas,(R_EAL g))) | [:I,J:])))) )
let f be PartFunc of [:[:RNS_Real,RNS_Real:],RNS_Real:],RNS_Real; :: thesis: for g being PartFunc of [:[:REAL,REAL:],REAL:],REAL st [:[:I,J:],K:] = dom f & f is_continuous_on [:[:I,J:],K:] & f = g holds
( ( for U being Element of L-Field holds Integral2 (L-Meas,(Integral2 (L-Meas,(R_EAL g)))) is U -measurable ) & Integral2 (L-Meas,(Integral2 (L-Meas,(R_EAL g)))) is_integrable_on L-Meas & Integral ((Prod_Measure (L-Meas,L-Meas)),(Integral2 (L-Meas,(R_EAL g)))) = Integral (L-Meas,(Integral2 (L-Meas,(Integral2 (L-Meas,(R_EAL g)))))) & Integral ((Prod_Measure ((Prod_Measure (L-Meas,L-Meas)),L-Meas)),g) = Integral (L-Meas,(Integral2 (L-Meas,(Integral2 (L-Meas,(R_EAL g)))))) & (Integral2 (L-Meas,(R_EAL g))) | [:I,J:] is_integrable_on Prod_Measure (L-Meas,L-Meas) & Integral ((Prod_Measure (L-Meas,L-Meas)),((Integral2 (L-Meas,(R_EAL g))) | [:I,J:])) = Integral (L-Meas,(Integral2 (L-Meas,((Integral2 (L-Meas,(R_EAL g))) | [:I,J:])))) )
let g be PartFunc of [:[:REAL,REAL:],REAL:],REAL; :: thesis: ( [:[:I,J:],K:] = dom f & f is_continuous_on [:[:I,J:],K:] & f = g implies ( ( for U being Element of L-Field holds Integral2 (L-Meas,(Integral2 (L-Meas,(R_EAL g)))) is U -measurable ) & Integral2 (L-Meas,(Integral2 (L-Meas,(R_EAL g)))) is_integrable_on L-Meas & Integral ((Prod_Measure (L-Meas,L-Meas)),(Integral2 (L-Meas,(R_EAL g)))) = Integral (L-Meas,(Integral2 (L-Meas,(Integral2 (L-Meas,(R_EAL g)))))) & Integral ((Prod_Measure ((Prod_Measure (L-Meas,L-Meas)),L-Meas)),g) = Integral (L-Meas,(Integral2 (L-Meas,(Integral2 (L-Meas,(R_EAL g)))))) & (Integral2 (L-Meas,(R_EAL g))) | [:I,J:] is_integrable_on Prod_Measure (L-Meas,L-Meas) & Integral ((Prod_Measure (L-Meas,L-Meas)),((Integral2 (L-Meas,(R_EAL g))) | [:I,J:])) = Integral (L-Meas,(Integral2 (L-Meas,((Integral2 (L-Meas,(R_EAL g))) | [:I,J:])))) ) )
assume that
A1: [:[:I,J:],K:] = dom f and
A2: f is_continuous_on [:[:I,J:],K:] and
A3: f = g ; :: thesis: ( ( for U being Element of L-Field holds Integral2 (L-Meas,(Integral2 (L-Meas,(R_EAL g)))) is U -measurable ) & Integral2 (L-Meas,(Integral2 (L-Meas,(R_EAL g)))) is_integrable_on L-Meas & Integral ((Prod_Measure (L-Meas,L-Meas)),(Integral2 (L-Meas,(R_EAL g)))) = Integral (L-Meas,(Integral2 (L-Meas,(Integral2 (L-Meas,(R_EAL g)))))) & Integral ((Prod_Measure ((Prod_Measure (L-Meas,L-Meas)),L-Meas)),g) = Integral (L-Meas,(Integral2 (L-Meas,(Integral2 (L-Meas,(R_EAL g)))))) & (Integral2 (L-Meas,(R_EAL g))) | [:I,J:] is_integrable_on Prod_Measure (L-Meas,L-Meas) & Integral ((Prod_Measure (L-Meas,L-Meas)),((Integral2 (L-Meas,(R_EAL g))) | [:I,J:])) = Integral (L-Meas,(Integral2 (L-Meas,((Integral2 (L-Meas,(R_EAL g))) | [:I,J:])))) )
set RF = Integral2 (L-Meas,(R_EAL g));
A4: dom (Integral2 (L-Meas,(R_EAL g))) = [:REAL,REAL:] by FUNCT_2:def 1;
reconsider RG = (Integral2 (L-Meas,(R_EAL g))) | [:I,J:] as PartFunc of [:REAL,REAL:],REAL by A1, A2, A3, Th32;
reconsider RGG = RG as PartFunc of [:RNS_Real,RNS_Real:],RNS_Real ;
A5: Integral2 (L-Meas,(R_EAL g)) is_integrable_on Prod_Measure (L-Meas,L-Meas) by A1, A2, A3, Th43;
A6: for x being Element of REAL holds (Integral2 (L-Meas,|.(Integral2 (L-Meas,(R_EAL g))).|)) . x < +infty by A1, A2, A3, Th46;
hence ( ( for U being Element of L-Field holds Integral2 (L-Meas,(Integral2 (L-Meas,(R_EAL g)))) is U -measurable ) & Integral2 (L-Meas,(Integral2 (L-Meas,(R_EAL g)))) is_integrable_on L-Meas & Integral ((Prod_Measure (L-Meas,L-Meas)),(Integral2 (L-Meas,(R_EAL g)))) = Integral (L-Meas,(Integral2 (L-Meas,(Integral2 (L-Meas,(R_EAL g)))))) ) by A5, MESFUN13:32, MESFUN16:5; :: thesis: ( Integral ((Prod_Measure ((Prod_Measure (L-Meas,L-Meas)),L-Meas)),g) = Integral (L-Meas,(Integral2 (L-Meas,(Integral2 (L-Meas,(R_EAL g)))))) & (Integral2 (L-Meas,(R_EAL g))) | [:I,J:] is_integrable_on Prod_Measure (L-Meas,L-Meas) & Integral ((Prod_Measure (L-Meas,L-Meas)),((Integral2 (L-Meas,(R_EAL g))) | [:I,J:])) = Integral (L-Meas,(Integral2 (L-Meas,((Integral2 (L-Meas,(R_EAL g))) | [:I,J:])))) )
A7: g is_integrable_on Prod_Measure ((Prod_Measure (L-Meas,L-Meas)),L-Meas) by A1, A2, A3, Th43;
for x being Element of [:REAL,REAL:] holds (Integral2 (L-Meas,|.(R_EAL g).|)) . x < +infty by A1, A2, A3, Th40;
then Integral ((Prod_Measure ((Prod_Measure (L-Meas,L-Meas)),L-Meas)),(R_EAL g)) = Integral ((Prod_Measure (L-Meas,L-Meas)),(Integral2 (L-Meas,(R_EAL g)))) by A7, MESFUN13:32, MESFUN16:5, MESFUN16:6;
hence Integral ((Prod_Measure ((Prod_Measure (L-Meas,L-Meas)),L-Meas)),g) = Integral (L-Meas,(Integral2 (L-Meas,(Integral2 (L-Meas,(R_EAL g)))))) by A5, A6, MESFUN13:32, MESFUN16:5; :: thesis: ( (Integral2 (L-Meas,(R_EAL g))) | [:I,J:] is_integrable_on Prod_Measure (L-Meas,L-Meas) & Integral ((Prod_Measure (L-Meas,L-Meas)),((Integral2 (L-Meas,(R_EAL g))) | [:I,J:])) = Integral (L-Meas,(Integral2 (L-Meas,((Integral2 (L-Meas,(R_EAL g))) | [:I,J:])))) )
A8: (Integral2 (L-Meas,(R_EAL g))) | [:I,J:] = R_EAL RG by MESFUNC5:def 7;
RGG is_uniformly_continuous_on [:I,J:] by A1, A2, A3, Th34;
then RGG is_continuous_on [:I,J:] by NFCONT_2:7;
then ( RG is_integrable_on Prod_Measure (L-Meas,L-Meas) & Integral ((Prod_Measure (L-Meas,L-Meas)),RG) = Integral (L-Meas,(Integral2 (L-Meas,(R_EAL RG)))) ) by A4, MESFUN16:57;
hence ( (Integral2 (L-Meas,(R_EAL g))) | [:I,J:] is_integrable_on Prod_Measure (L-Meas,L-Meas) & Integral ((Prod_Measure (L-Meas,L-Meas)),((Integral2 (L-Meas,(R_EAL g))) | [:I,J:])) = Integral (L-Meas,(Integral2 (L-Meas,((Integral2 (L-Meas,(R_EAL g))) | [:I,J:])))) ) by A8; :: thesis: verum