theorem Th75: :: MEASUR11:76

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 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 C being summable FinSequence of Funcs ([:X1,X2:],ExtREAL) ex I being summable FinSequence of Funcs (X1,ExtREAL) ex J being summable FinSequence of Funcs (X2,ExtREAL) st
( E = Union F & len F in dom F & len F = len A & len F = len B & len F = len C & len F = len I & len F = len J & ( for n being Nat st n in dom C holds
C . n = chi ((F . n),[:X1,X2:]) ) & (Partial_Sums C) /. (len C) = chi (E,[:X1,X2:]) & ( for x being Element of X1
for n being Nat st n in dom I holds
(I . n) . x = Integral (M2,(ProjMap1 ((C /. n),x))) ) & ( for n being Nat
for P being Element of S1 st n in dom I holds
I /. n is P -measurable ) & ( for x being Element of X1 holds Integral (M2,(ProjMap1 (((Partial_Sums C) /. (len C)),x))) = ((Partial_Sums I) /. (len I)) . x ) & ( for y being Element of X2
for n being Nat st n in dom J holds
(J . n) . y = Integral (M1,(ProjMap2 ((C /. n),y))) ) & ( for n being Nat
for P being Element of S2 st n in dom J holds
J /. n is P -measurable ) & ( for y being Element of X2 holds Integral (M1,(ProjMap2 (((Partial_Sums C) /. (len C)),y))) = ((Partial_Sums J) /. (len J)) . y ) )