let n be non zero Nat; Prod_Measure (L-Meas (n + 1)) = Prod_Measure ((Prod_Measure (L-Meas n)),L-Meas)
set X = (Seg (n + 1)) --> REAL;
set S = L-Field (n + 1);
set m = L-Meas (n + 1);
set X1 = SubFin (((Seg (n + 1)) --> REAL),n);
set S1 = SubFin ((L-Field (n + 1)),n);
set m1 = SubFin ((L-Meas (n + 1)),n);
set X11 = ElmFin (((Seg (n + 1)) --> REAL),(n + 1));
set S11 = ElmFin ((L-Field (n + 1)),(n + 1));
set m11 = ElmFin ((L-Meas (n + 1)),(n + 1));
A1:
Prod_Measure (L-Meas (n + 1)) = Prod_Measure ((Prod_Measure (SubFin ((L-Meas (n + 1)),n))),(ElmFin ((L-Meas (n + 1)),(n + 1))))
by MEASUR13:28;
A2:
Seg n c= Seg (n + 1)
by NAT_1:12, FINSEQ_1:5;
SubFin (((Seg (n + 1)) --> REAL),n) = ((Seg (n + 1)) --> REAL) | n
by NAT_1:12, MEASUR13:def 5;
then
SubFin (((Seg (n + 1)) --> REAL),n) = ((Seg (n + 1)) /\ (Seg n)) --> REAL
by FUNCOP_1:12;
then A3:
SubFin (((Seg (n + 1)) --> REAL),n) = (Seg n) --> REAL
by A2, XBOOLE_1:28;
SubFin ((L-Field (n + 1)),n) = (L-Field (n + 1)) | n
by NAT_1:12, MEASUR13:def 6;
then
SubFin ((L-Field (n + 1)),n) = ((Seg (n + 1)) /\ (Seg n)) --> L-Field
by FUNCOP_1:12;
then A4:
SubFin ((L-Field (n + 1)),n) = L-Field n
by A2, XBOOLE_1:28;
SubFin ((L-Meas (n + 1)),n) = (L-Meas (n + 1)) | n
by NAT_1:12, MEASUR13:def 9;
then
SubFin ((L-Meas (n + 1)),n) = ((Seg (n + 1)) /\ (Seg n)) --> L-Meas
by FUNCOP_1:12;
then A5:
SubFin ((L-Meas (n + 1)),n) = L-Meas n
by A2, XBOOLE_1:28;
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 FUNCOP_1:7, FINSEQ_1:3;
ElmFin ((L-Field (n + 1)),(n + 1)) = (L-Field (n + 1)) . (n + 1)
by MEASUR13:def 7;
then A7:
ElmFin ((L-Field (n + 1)),(n + 1)) = L-Field
by FUNCOP_1:7, FINSEQ_1:3;
ElmFin ((L-Meas (n + 1)),(n + 1)) = (L-Meas (n + 1)) . (n + 1)
by MEASUR13:def 10;
hence
Prod_Measure (L-Meas (n + 1)) = Prod_Measure ((Prod_Measure (L-Meas n)),L-Meas)
by A7, A1, A4, A3, A5, A6, FUNCOP_1:7, FINSEQ_1:3; verum