theorem Th49: :: MESFUN18:49

for n being non zero Nat
for D being b₁ -element FinSequence
for I being Subset of (CarProduct ((Seg n) --> RNS_Real))
for J being Interval st ( for i being Nat st i in Seg n holds
D . i is Interval ) & I = CarProduct D holds
( [:I,J:] is Subset of [:(CarProduct ((Seg n) --> RNS_Real)),RNS_Real:] & [:I,J:] in sigma (measurable_rectangles ((Prod_Field (L-Field n)),L-Field)) )