theorem Th34: :: MEASUR13:34

for n being non zero Nat
for X being non-empty b₁ + 1 -element FinSequence
for S being sigmaFieldFamily of X
for M being sigmaMeasureFamily of S holds Prod_Field S = sigma (measurable_rectangles ((Prod_Field (SubFin (S,n))),(ElmFin (S,(n + 1)))))