theorem :: MEASUR14:35

for n being non zero Nat
for X being non-empty b₁ -element FinSequence
for S being sigmaFieldFamily of X
for m being sigmaMeasureFamily of S
for f being PartFunc of (CarProduct X),ExtREAL
for g being PartFunc of (product X),ExtREAL
for A being Element of Prod_Field S st g = f * ((CarProd X) ") & A = dom f & f is A -measurable holds
Integral ((XProd_Measure m),g) = Integral ((Prod_Measure m),f) by Th12, Th32;