let n be non zero Nat; :: thesis: Prod_Field (L-Field (n + 1)) = sigma (measurable_rectangles ((Prod_Field (L-Field n)),L-Field))
set X = (Seg (n + 1)) --> REAL;
set X1 = SubFin (((Seg (n + 1)) --> REAL),n);
set S1 = SubFin ((L-Field (n + 1)),n);
set S11 = ElmFin ((L-Field (n + 1)),(n + 1));
A1: Prod_Field (L-Field (n + 1)) = sigma (measurable_rectangles ((Prod_Field (SubFin ((L-Field (n + 1)),n))),(ElmFin ((L-Field (n + 1)),(n + 1))))) by MEASUR13:34;
A2: n < n + 1 by NAT_1:13;
then A3: (Seg (n + 1)) /\ (Seg n) = Seg n by FINSEQ_1:5, XBOOLE_1:28;
SubFin (((Seg (n + 1)) --> REAL),n) = ((Seg (n + 1)) --> REAL) | n by A2, MEASUR13:def 5;
then A4: SubFin (((Seg (n + 1)) --> REAL),n) = (Seg n) --> REAL by A3, FUNCOP_1:12;
SubFin ((L-Field (n + 1)),n) = (L-Field (n + 1)) | n by A2, MEASUR13:def 6;
then A5: SubFin ((L-Field (n + 1)),n) = L-Field n by A3, FUNCOP_1:12;
ElmFin (((Seg (n + 1)) --> REAL),(n + 1)) = ((Seg (n + 1)) --> REAL) . (n + 1) by MEASUR13:def 1;
then A6: ElmFin (((Seg (n + 1)) --> REAL),(n + 1)) = REAL by FINSEQ_1:4, FUNCOP_1:7;
ElmFin ((L-Field (n + 1)),(n + 1)) = (L-Field (n + 1)) . (n + 1) by MEASUR13:def 7;
hence Prod_Field (L-Field (n + 1)) = sigma (measurable_rectangles ((Prod_Field (L-Field n)),L-Field)) by A1, A4, A5, A6, FINSEQ_1:4, FUNCOP_1:7; :: thesis: verum