theorem :: MESFUN16:57

for I, J being non empty closed_interval Subset of REAL
for f being PartFunc of [:RNS_Real,RNS_Real:],RNS_Real
for g being PartFunc of [:REAL,REAL:],REAL st [:I,J:] = dom f & f is_continuous_on [:I,J:] & f = g holds
( g is_integrable_on Prod_Measure (L-Meas,L-Meas) & ( for x being Element of REAL holds (Integral2 (L-Meas,|.(R_EAL g).|)) . x < +infty ) & ( for y being Element of REAL holds (Integral1 (L-Meas,|.(R_EAL g).|)) . y < +infty ) & ( for U being Element of L-Field holds Integral2 (L-Meas,(R_EAL g)) is U -measurable ) & ( for V being Element of L-Field holds Integral1 (L-Meas,(R_EAL g)) is V -measurable ) & Integral2 (L-Meas,(R_EAL g)) is_integrable_on L-Meas & Integral1 (L-Meas,(R_EAL g)) is_integrable_on L-Meas & Integral ((Prod_Measure (L-Meas,L-Meas)),g) = Integral (L-Meas,(Integral2 (L-Meas,(R_EAL g)))) & Integral ((Prod_Measure (L-Meas,L-Meas)),g) = Integral (L-Meas,(Integral1 (L-Meas,(R_EAL g)))) ) by Lm4, Lm5;