theorem Th70: :: MEASUR11:74

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)) & E <> {} holds
ex f being disjoint_valued FinSequence of measurable_rectangles (S1,S2) ex A being FinSequence of S1 ex B being FinSequence of S2 ex Xf being summable FinSequence of Funcs ([:X1,X2:],ExtREAL) st
( E = Union f & len f in dom f & len f = len A & len f = len B & len f = len Xf & ( for n being Nat st n in dom f holds
f . n = [:(A . n),(B . n):] ) & ( for n being Nat st n in dom Xf holds
Xf . n = chi ((f . n),[:X1,X2:]) ) & (Partial_Sums Xf) . (len Xf) = chi (E,[:X1,X2:]) & ( for n being Nat
for x, y being set st n in dom Xf & x in X1 & y in X2 holds
(Xf . n) . (x,y) = ((chi ((A . n),X1)) . x) * ((chi ((B . n),X2)) . y) ) & ( for x being Element of X1 holds ProjMap1 ((chi (E,[:X1,X2:])),x) = ProjMap1 (((Partial_Sums Xf) /. (len Xf)),x) ) & ( for y being Element of X2 holds ProjMap2 ((chi (E,[:X1,X2:])),y) = ProjMap2 (((Partial_Sums Xf) /. (len Xf)),y) ) )