theorem Th31: :: MESFUN12:31

for X1, X2 being non empty set
for S1 being SigmaField of X1
for S2 being SigmaField of X2
for x being Element of X1
for y being Element of X2
for f being PartFunc of [:X1,X2:],ExtREAL st f is_simple_func_in sigma (measurable_rectangles (S1,S2)) holds
( ProjPMap1 (f,x) is_simple_func_in S2 & ProjPMap2 (f,y) is_simple_func_in S1 )