theorem Th34: :: MEASUR14:34

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
for B being Element of XProd_Field S st B = (CarProd X) .: A & g = f * ((CarProd X) ") holds
( f is A -measurable iff g is B -measurable )