theorem Th21: :: MEASUR13:21

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