theorem Th109: :: MEASUR11:109

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 E, V being Element of sigma (measurable_rectangles (S1,S2))
for P being Set_Sequence of sigma (measurable_rectangles (S1,S2))
for y being Element of X2 st P is non-descending & lim P = E holds
ex K being SetSequence of S1 st
( K is non-descending & ( for n being Nat holds K . n = (Measurable-Y-section ((P . n),y)) /\ (Measurable-Y-section (V,y)) ) & lim K = (Measurable-Y-section (E,y)) /\ (Measurable-Y-section (V,y)) )