set X = (Seg 2) --> REAL;
set S = L-Field 2;
set m = L-Meas 2;
set X1 = SubFin (((Seg 2) --> REAL),1);
set S1 = SubFin ((L-Field 2),1);
set m1 = SubFin ((L-Meas 2),1);
set X11 = ElmFin (((Seg 2) --> REAL),2);
set S11 = ElmFin ((L-Field 2),2);
set m11 = ElmFin ((L-Meas 2),(1 + 1));
A1: Prod_Measure (L-Meas 2) = product_sigma_Measure ((Prod_Measure (SubFin ((L-Meas 2),1))),(ElmFin ((L-Meas 2),(1 + 1)))) by MEASUR13:25;
A2: ( 1 in Seg 1 & 1 in Seg 2 & 2 in Seg 2 ) ;
( ElmFin ((L-Field 2),2) = (L-Field 2) . 2 & ElmFin ((L-Meas 2),(1 + 1)) = (L-Meas 2) . 2 ) by MEASUR13:def 7, MEASUR13:def 10;
then A3: ( ElmFin ((L-Field 2),2) = L-Field & ElmFin ((L-Meas 2),(1 + 1)) = L-Meas ) by A2, FUNCOP_1:7;
A4: ( len (SubFin (((Seg 2) --> REAL),1)) = 1 & len (SubFin ((L-Field 2),1)) = 1 & len (SubFin ((L-Meas 2),1)) = 1 ) by CARD_1:def 7;
( SubFin (((Seg 2) --> REAL),1) = ((Seg 2) --> REAL) | 1 & SubFin ((L-Field 2),1) = (L-Field 2) | 1 & SubFin ((L-Meas 2),1) = (L-Meas 2) | 1 ) by MEASUR13:def 5, MEASUR13:def 6, MEASUR13:def 9;
then ( (SubFin (((Seg 2) --> REAL),1)) . 1 = ((Seg 2) --> REAL) . 1 & (SubFin ((L-Field 2),1)) . 1 = (L-Field 2) . 1 & (SubFin ((L-Meas 2),1)) . 1 = (L-Meas 2) . 1 ) by A2, FUNCT_1:49;
then ( SubFin (((Seg 2) --> REAL),1) = <*REAL*> & SubFin ((L-Field 2),1) = <*L-Field*> & SubFin ((L-Meas 2),1) = <*L-Meas*> ) by A4, A2, FUNCOP_1:7, FINSEQ_1:40;
then A5: ( SubFin (((Seg 2) --> REAL),1) = 1 |-> REAL & SubFin ((L-Field 2),1) = 1 |-> L-Field & SubFin ((L-Meas 2),1) = 1 |-> L-Meas ) by FINSEQ_2:59;
hence Prod_Measure (L-Meas 2) = Prod_Measure (L-Meas,L-Meas) by A1, A3, Th37, Th41, Th45, MESFUN12:def 9; :: thesis: for E1, E2 being Element of L-Field holds
( [:E1,E2:] in measurable_rectangles (L-Field,L-Field) & (Prod_Measure (L-Meas 2)) . [:E1,E2:] = (L-Meas . E1) * (L-Meas . E2) )
thus for E1, E2 being Element of L-Field holds
( [:E1,E2:] in measurable_rectangles (L-Field,L-Field) & (Prod_Measure (L-Meas 2)) . [:E1,E2:] = (L-Meas . E1) * (L-Meas . E2) ) :: thesis: verum

proof

let E1, E2 be Element of L-Field ; :: thesis: ( [:E1,E2:] in measurable_rectangles (L-Field,L-Field) & (Prod_Measure (L-Meas 2)) . [:E1,E2:] = (L-Meas . E1) * (L-Meas . E2) )
A6: [:E1,E2:] in measurable_rectangles (L-Field,L-Field) ;
measurable_rectangles (L-Field,L-Field) c= sigma (measurable_rectangles (L-Field,L-Field)) by PROB_1:def 9;
then reconsider E = [:E1,E2:] as Element of sigma (measurable_rectangles (L-Field,L-Field)) by A6;
(product_sigma_Measure (L-Meas,L-Meas)) . E = (L-Meas . E1) * (L-Meas . E2) by MEASUR11:16;
hence ( [:E1,E2:] in measurable_rectangles (L-Field,L-Field) & (Prod_Measure (L-Meas 2)) . [:E1,E2:] = (L-Meas . E1) * (L-Meas . E2) ) by A5, A3, Th37, Th41, Th45, MEASUR13:25; :: thesis: verum

end;