let n be non zero Nat; :: thesis:
let D be n + 1 -element FinSequence; :: thesis:
let f be PartFunc of (REAL-NS (n + 1)),RNS_Real; :: thesis:
let G be PartFunc of (CarProduct ((Seg (n + 1)) --> REAL)),REAL; :: thesis:
let g0 be PartFunc of [:(CarProduct ((Seg n) --> REAL)),REAL:],REAL; :: thesis:
assume that
A1: for i being Nat st i in Seg (n + 1) holds
D . i is closed_interval Subset of REAL and
A2: f is_continuous_on product D and
A3: dom f = product D and
A4: G = f * (CarProd ((Seg (n + 1)) --> REAL)) and
A5: g0 = G ; :: thesis:
set I = CarProd ((Seg (n + 1)) --> RNS_Real);
set I0 = CarProd ((Seg (n + 1)) --> REAL);
A6: ex CX being non-empty n + 1 -element FinSequence st
( CX = carr ((Seg (n + 1)) --> RNS_Real) & CarProduct CX = the carrier of (CarProduct ((Seg (n + 1)) --> RNS_Real)) & CarProd ((Seg (n + 1)) --> RNS_Real) = CarProd CX & CarProd ((Seg (n + 1)) --> RNS_Real) is bijective ) by MEASUR15:def 7;
A7: CarProd ((Seg (n + 1)) --> RNS_Real) = CarProd ((Seg (n + 1)) --> REAL) by MEASUR15:70;
A8: for i being Nat st i in Seg (n + 1) holds
D . i c= REAL

let i be Nat; :: thesis:
assume i in Seg (n + 1) ; :: thesis:
then D . i is Subset of REAL by A1;
hence D . i c= REAL ; :: thesis:

end;

for i being Nat st i in Seg (n + 1) holds
D . i c= ((Seg (n + 1)) --> REAL) . i

let i be Nat; :: thesis:
assume A9: i in Seg (n + 1) ; :: thesis:
then A10: D . i is Subset of REAL by A1;
((Seg (n + 1)) --> REAL) . i = REAL by A9, FUNCOP_1:7;
hence D . i c= ((Seg (n + 1)) --> REAL) . i by A10; :: thesis:

end;

then CarProduct D c= CarProduct ((Seg (n + 1)) --> REAL) by Th10;
then CarProduct D c= the carrier of (CarProduct ((Seg (n + 1)) --> RNS_Real)) by MEASUR15:42;
then A11: CarProduct D c= dom (CarProd ((Seg (n + 1)) --> RNS_Real)) by FUNCT_2:def 1;
reconsider D1 = D | n as n -element FinSequence ;
for i being Nat st i in Seg n holds
D1 . i c= ((Seg n) --> REAL) . i

let i be Nat; :: thesis:
assume A12: i in Seg n ; :: thesis:
then A13: i <= n by FINSEQ_1:1;
A14: Seg n c= Seg (n + 1) by FINSEQ_3:18;
D1 . i = D . i by A13, FINSEQ_3:112;
then A15: D1 . i is Subset of REAL by A1, A12, A14;
((Seg n) --> REAL) . i = REAL by A12, FUNCOP_1:7;
hence D1 . i c= ((Seg n) --> REAL) . i by A15; :: thesis:

end;

then A16: CarProduct D1 is Subset of (CarProduct ((Seg n) --> REAL)) by Th10;
then reconsider I1 = CarProduct D1 as Subset of (CarProduct ((Seg n) --> RNS_Real)) by MEASUR15:42;
reconsider J1 = D . (n + 1) as closed_interval Subset of REAL by A1, FINSEQ_1:4;
reconsider f0 = f * (CarProd ((Seg (n + 1)) --> RNS_Real)) as PartFunc of [:(CarProduct ((Seg n) --> RNS_Real)),RNS_Real:],RNS_Real by MEASUR15:38;
A17: for i being Nat st i in Seg (n + 1) holds
D . i is Subset of REAL by A1;
then A18: f * (CarProd ((Seg (n + 1)) --> RNS_Real)) is_continuous_on CarProduct D by A2, A3, Th62;
A19: CarProduct D = [:(CarProduct D1),(D . (n + 1)):] by Th4;
dom (f * (CarProd ((Seg (n + 1)) --> RNS_Real))) = (CarProd ((Seg (n + 1)) --> RNS_Real)) " (product D) by A3, RELAT_1:147;
then dom (f * (CarProd ((Seg (n + 1)) --> RNS_Real))) = (CarProd ((Seg (n + 1)) --> RNS_Real)) " ((CarProd ((Seg (n + 1)) --> RNS_Real)) .: (CarProduct D)) by A8, A7, Th12;
then A20: dom (f * (CarProd ((Seg (n + 1)) --> RNS_Real))) = CarProduct D by A6, A11, FUNCT_1:94;
then A21: dom f0 = [:I1,J1:] by Th4;
A22: CarProduct ((Seg (n + 1)) --> RNS_Real) = [:(CarProduct ((Seg n) --> RNS_Real)),RNS_Real:] by MEASUR15:38;
A23: for i being Nat st i in Seg n holds
D1 . i is closed_interval Subset of REAL

let i be Nat; :: thesis:
assume A24: i in Seg n ; :: thesis:
then i <= n by FINSEQ_1:1;
then A25: D1 . i = D . i by FINSEQ_3:112;
Seg n c= Seg (n + 1) by FINSEQ_3:18;
hence D1 . i is closed_interval Subset of REAL by A1, A24, A25; :: thesis:

end;

hence for x being Element of CarProduct ((Seg n) --> REAL) holds (Integral2 (L-Meas,|.(R_EAL g0).|)) . x < +infty by A5, A4, A7, A18, A22, A21, A19, Lm3; :: thesis:
thus for x being Element of CarProduct ((Seg n) --> REAL) holds ProjPMap1 ((R_EAL g0),x) is_integrable_on L-Meas :: thesis:

let x be Element of CarProduct ((Seg n) --> REAL); :: thesis:
reconsider Pg1 = ProjPMap1 ((R_EAL g0),x) as PartFunc of REAL,REAL by MESFUN16:30;
Pg1 is_integrable_on L-Meas by A16, A5, A4, A7, A21, A17, A2, A3, A22, A19, Th29, Th62;
hence ProjPMap1 ((R_EAL g0),x) is_integrable_on L-Meas by MESFUNC5:def 7; :: thesis:

end;

Integral ((Prod_Measure (L-Meas (n + 1))),G) = Integral ((Prod_Measure ((Prod_Measure (L-Meas n)),L-Meas)),g0) by A1, A5, A4, A7, A20, A18, Th56;
hence ( ( for U being Element of Prod_Field (L-Field n) holds Integral2 (L-Meas,(R_EAL g0)) is U -measurable ) & Integral2 (L-Meas,(R_EAL g0)) is_integrable_on Prod_Measure (L-Meas n) & Integral ((Prod_Measure (L-Meas (n + 1))),G) = Integral ((Prod_Measure (L-Meas n)),(Integral2 (L-Meas,(R_EAL g0)))) ) by A5, A4, A7, A21, A18, A22, A19, A23, Lm3; :: thesis: