theorem Th44: :: MEASUR14:44

for n being non zero Nat holds Prod_Field (L-Field (n + 1)) = sigma (measurable_rectangles ((Prod_Field (L-Field n)),L-Field))