set X = (Seg 3) --> REAL;
set S = L-Field 3;
set m = L-Meas 3;
set X2 = SubFin (((Seg 3) --> REAL),2);
set S2 = SubFin ((L-Field 3),2);
set m2 = SubFin ((L-Meas 3),2);
set X21 = ElmFin (((Seg 3) --> REAL),3);
set S21 = ElmFin ((L-Field 3),3);
set m21 = ElmFin ((L-Meas 3),(2 + 1));
A1: Prod_Measure (L-Meas 3) = product_sigma_Measure ((Prod_Measure (SubFin ((L-Meas 3),2))),(ElmFin ((L-Meas 3),(2 + 1)))) by MEASUR13:25;
A2: ( 1 in Seg 2 & 2 in Seg 2 & 1 in Seg 3 & 2 in Seg 3 & 3 in Seg 3 ) ;
( ElmFin (((Seg 3) --> REAL),3) = ((Seg 3) --> REAL) . 3 & ElmFin ((L-Field 3),3) = (L-Field 3) . 3 & ElmFin ((L-Meas 3),(2 + 1)) = (L-Meas 3) . 3 ) by MEASUR13:def 1, MEASUR13:def 7, MEASUR13:def 10;
then A3: ( ElmFin (((Seg 3) --> REAL),3) = REAL & ElmFin ((L-Field 3),3) = L-Field & ElmFin ((L-Meas 3),(2 + 1)) = L-Meas ) by A2, FUNCOP_1:7;
A4: ( len (SubFin (((Seg 3) --> REAL),2)) = 2 & len (SubFin ((L-Field 3),2)) = 2 & len (SubFin ((L-Meas 3),2)) = 2 ) by CARD_1:def 7;
A5: SubFin (((Seg 3) --> REAL),2) = ((Seg 3) --> REAL) | 2 by MEASUR13:def 5;
then (SubFin (((Seg 3) --> REAL),2)) . 1 = ((Seg 3) --> REAL) . 1 by A2, FUNCT_1:49;
then A6: (SubFin (((Seg 3) --> REAL),2)) . 1 = REAL by FUNCOP_1:7, A2;
(SubFin (((Seg 3) --> REAL),2)) . 2 = ((Seg 3) --> REAL) . 2 by A2, A5, FUNCT_1:49;
then SubFin (((Seg 3) --> REAL),2) = <*REAL,REAL*> by A4, A6, A2, FUNCOP_1:7, FINSEQ_1:44;
then A7: SubFin (((Seg 3) --> REAL),2) = 2 |-> REAL by FINSEQ_2:61;
A8: SubFin ((L-Field 3),2) = (L-Field 3) | 2 by MEASUR13:def 6;
then (SubFin ((L-Field 3),2)) . 1 = (L-Field 3) . 1 by A2, FUNCT_1:49;
then A9: (SubFin ((L-Field 3),2)) . 1 = L-Field by A2, FUNCOP_1:7;
(SubFin ((L-Field 3),2)) . 2 = (L-Field 3) . 2 by A2, A8, FUNCT_1:49;
then SubFin ((L-Field 3),2) = <*L-Field,L-Field*> by A4, A9, A2, FUNCOP_1:7, FINSEQ_1:44;
then A10: SubFin ((L-Field 3),2) = 2 |-> L-Field by FINSEQ_2:61;
A11: SubFin ((L-Meas 3),2) = (L-Meas 3) | 2 by MEASUR13:def 9;
then (SubFin ((L-Meas 3),2)) . 1 = (L-Meas 3) . 1 by A2, FUNCT_1:49;
then A12: (SubFin ((L-Meas 3),2)) . 1 = L-Meas by A2, FUNCOP_1:7;
(SubFin ((L-Meas 3),2)) . 2 = (L-Meas 3) . 2 by A2, A11, FUNCT_1:49;
then SubFin ((L-Meas 3),2) = <*L-Meas,L-Meas*> by A4, A12, A2, FUNCOP_1:7, FINSEQ_1:44;
then SubFin ((L-Meas 3),2) = 2 |-> L-Meas by FINSEQ_2:61;
hence A13: Prod_Measure (L-Meas 3) = Prod_Measure ((Prod_Measure (L-Meas,L-Meas)),L-Meas) by A1, A7, A10, A3, Th37, Th42, Th46, MESFUN12:def 9; :: thesis:
thus for E1, E2, E3 being Element of L-Field holds
( [:E1,E2,E3:] in measurable_rectangles ((sigma (measurable_rectangles (L-Field,L-Field))),L-Field) & (Prod_Measure (L-Meas 3)) . [:E1,E2,E3:] = ((L-Meas . E1) * (L-Meas . E2)) * (L-Meas . E3) ) :: thesis:

let E1, E2, E3 be Element of L-Field ; :: thesis:
measurable_rectangles (L-Field,L-Field) c= sigma (measurable_rectangles (L-Field,L-Field)) by PROB_1:def 9;
then reconsider F = [:E1,E2:] as Element of sigma (measurable_rectangles (L-Field,L-Field)) by Th46;
A14: [:F,E3:] in measurable_rectangles ((sigma (measurable_rectangles (L-Field,L-Field))),L-Field) ;
hence [:E1,E2,E3:] in measurable_rectangles ((sigma (measurable_rectangles (L-Field,L-Field))),L-Field) by ZFMISC_1:def 3; :: thesis:
measurable_rectangles ((sigma (measurable_rectangles (L-Field,L-Field))),L-Field) c= sigma (measurable_rectangles ((sigma (measurable_rectangles (L-Field,L-Field))),L-Field)) by PROB_1:def 9;
then (product_sigma_Measure ((Prod_Measure (L-Meas,L-Meas)),L-Meas)) . [:F,E3:] = ((Prod_Measure (L-Meas,L-Meas)) . F) * (L-Meas . E3) by A14, MEASUR11:16
.= ((L-Meas . E1) * (L-Meas . E2)) * (L-Meas . E3) by Th46 ;
then (Prod_Measure ((Prod_Measure (L-Meas,L-Meas)),L-Meas)) . [:F,E3:] = ((L-Meas . E1) * (L-Meas . E2)) * (L-Meas . E3) by MESFUN12:def 9;
hence (Prod_Measure (L-Meas 3)) . [:E1,E2,E3:] = ((L-Meas . E1) * (L-Meas . E2)) * (L-Meas . E3) by A13, ZFMISC_1:def 3; :: thesis:

end;