let n be non zero Nat; :: thesis: 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) )
let E1 be Element of Prod_Field (L-Field n); :: thesis: 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) )
let E2 be Element of L-Field ; :: thesis: ( [: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) )
A1: [:E1,E2:] in measurable_rectangles ((Prod_Field (L-Field n)),L-Field) ;
A2: measurable_rectangles ((Prod_Field (L-Field n)),L-Field) c= sigma (measurable_rectangles ((Prod_Field (L-Field n)),L-Field)) by PROB_1:def 9;
hence [:E1,E2:] in sigma (measurable_rectangles ((Prod_Field (L-Field n)),L-Field)) by A1; :: thesis: (Prod_Measure (L-Meas (n + 1))) . [:E1,E2:] = ((Prod_Measure (L-Meas n)) . E1) * (L-Meas . E2)
reconsider E = [:E1,E2:] as Element of sigma (measurable_rectangles ((Prod_Field (L-Field n)),L-Field)) by A1, A2;
(product_sigma_Measure ((Prod_Measure (L-Meas n)),L-Meas)) . E = ((Prod_Measure (L-Meas n)) . E1) * (L-Meas . E2) by MEASUR11:16;
then (Prod_Measure ((Prod_Measure (L-Meas n)),L-Meas)) . E = ((Prod_Measure (L-Meas n)) . E1) * (L-Meas . E2) by MESFUN12:def 9;
hence (Prod_Measure (L-Meas (n + 1))) . [:E1,E2:] = ((Prod_Measure (L-Meas n)) . E1) * (L-Meas . E2) by MEASUR14:48; :: thesis: verum