theorem Th51: :: MESFUN18:51

for n being non zero Nat
for E1 being Element of Prod_Field (L-Field n)
for E2 being Element of L-Field holds
( [:E1,E2:] in sigma (measurable_rectangles ((Prod_Field (L-Field n)),L-Field)) & (Prod_Measure (L-Meas (n + 1))) . [:E1,E2:] = ((Prod_Measure (L-Meas n)) . E1) * (L-Meas . E2) )