theorem Th29: :: MEASUR13:29

for m being non zero Nat
for X being non-empty b₁ -element FinSequence
for S being sigmaFieldFamily of X
for M being sigmaMeasureFamily of S st M is sigma_finite holds
Prod_Measure M is sigma_finite