theorem :: MESFUN17:44

for I, J, K being non empty closed_interval Subset of REAL
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 z being Element of REAL holds ProjPMap2 ((R_EAL g),z) is_integrable_on Prod_Measure (L-Meas,L-Meas) ) & ( for V being Element of L-Field holds Integral1 ((Prod_Measure (L-Meas,L-Meas)),(R_EAL g)) is V -measurable ) & Integral1 ((Prod_Measure (L-Meas,L-Meas)),(R_EAL g)) is_integrable_on L-Meas & Integral ((Prod_Measure ((Prod_Measure (L-Meas,L-Meas)),L-Meas)),g) = Integral (L-Meas,(Integral1 ((Prod_Measure (L-Meas,L-Meas)),(R_EAL g)))) )