theorem Th66: :: MEASUR11:70

for X1, X2 being non empty set
for S1 being SigmaField of X1
for S2 being SigmaField of X2
for E being Element of sigma (measurable_rectangles (S1,S2)) st E in Field_generated_by (measurable_rectangles (S1,S2)) holds
ex f being disjoint_valued FinSequence of measurable_rectangles (S1,S2) ex A being FinSequence of S1 ex B being FinSequence of S2 st
( len f = len A & len f = len B & E = Union f & ( for n being Nat st n in dom f holds
( proj1 (f . n) = A . n & proj2 (f . n) = B . n ) ) & ( for n being Nat
for x, y being set st n in dom f & x in X1 & y in X2 holds
(chi ((f . n),[:X1,X2:])) . (x,y) = ((chi ((A . n),X1)) . x) * ((chi ((B . n),X2)) . y) ) )