for X1, X2 being non empty set
for S1 being SigmaField of X1
for S2 being SigmaField of X2
for M1 being sigma_Measure of S1
for M2 being sigma_Measure of S2
for f being PartFunc of [:X1,X2:],ExtREAL
for SX1 being Element of S1 st M1 is sigma_finite & M2 is sigma_finite & f is_integrable_on Prod_Measure (M1,M2) & X1 = SX1 holds
ex U being Element of S1 st
( M1 . U = 0 & ( for x being Element of X1 st x in U ` holds
ProjPMap1 (f,x) is_integrable_on M2 ) & (Integral2 (M2,|.f.|)) | (U `) is PartFunc of X1,REAL & Integral2 (M2,f) is SX1 \ U -measurable & (Integral2 (M2,f)) | (U `) is_integrable_on M1 & (Integral2 (M2,f)) | (U `) in L1_Functions M1 & ex g being Function of X1,ExtREAL st
( g is_integrable_on M1 & g | (U `) = (Integral2 (M2,f)) | (U `) & Integral ((Prod_Measure (M1,M2)),f) = Integral (M1,g) ) )