theorem Th30: :: MEASUR10:30

for X1, X2 being non empty set
for S1 being SigmaField of X1
for S2 being SigmaField of X2
for M2 being sigma_Measure of S2
for D being Function of NAT,S1
for E being Function of NAT,S2
for A being Element of S1
for B being Element of S2
for F being Functional_Sequence of X2,ExtREAL
for RD being sequence of (Funcs (X1,REAL))
for x being Element of X1 st ( for n being Nat holds RD . n = chi ((D . n),X1) ) & ( for n being Nat holds F . n = ((RD . n) . x) (#) (chi ((E . n),X2)) ) & ( for n being Nat holds E . n c= B ) holds
ex I being ExtREAL_sequence st
( ( for n being Nat holds I . n = (M2 . (E . n)) * ((chi ((D . n),X1)) . x) ) & I is summable & Integral (M2,(lim (Partial_Sums F))) = Sum I )