let n be non zero Nat; :: thesis:
let D be n + 1 -element FinSequence; :: thesis:
let D1 be n -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:
let Dk1 be non empty closed_interval Subset of REAL; :: thesis:
let x be Element of CarProduct ((Seg n) --> REAL); :: thesis:
let Pg be PartFunc of REAL,REAL; :: thesis:
assume that
A1: D1 = D | n and
A2: for i being Nat st i in Seg (n + 1) holds
D . i is Subset of REAL and
A3: f is_continuous_on product D and
A4: dom f = product D and
A5: G = f * (CarProd ((Seg (n + 1)) --> REAL)) and
A6: g0 = G and
A7: Dk1 = D . (n + 1) and
A8: x in CarProduct D1 and
A9: Pg = ProjPMap1 (|.(R_EAL g0).|,x) ; :: thesis:
set I = CarProd ((Seg (n + 1)) --> RNS_Real);
set I0 = CarProd ((Seg (n + 1)) --> REAL);
A10: 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;
A11: CarProd ((Seg (n + 1)) --> RNS_Real) = CarProd ((Seg (n + 1)) --> REAL) by MEASUR15:70;
A12: 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 A2;
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 A13: i in Seg (n + 1) ; :: thesis:
then D . i is Subset of REAL by A2;
then D . i c= REAL ;
hence D . i c= ((Seg (n + 1)) --> REAL) . i by A13, FUNCOP_1:7; :: 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 A14: CarProduct D c= dom (CarProd ((Seg (n + 1)) --> RNS_Real)) by FUNCT_2:def 1;
dom (f * (CarProd ((Seg (n + 1)) --> RNS_Real))) = (CarProd ((Seg (n + 1)) --> RNS_Real)) " (product D) by A4, 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 A12, A11, Th12;
then A15: dom (f * (CarProd ((Seg (n + 1)) --> RNS_Real))) = CarProduct D by A10, A14, FUNCT_1:94;
A16: f * (CarProd ((Seg (n + 1)) --> RNS_Real)) is_continuous_on CarProduct D by A2, A3, A4, Th62;
for i being Nat st i in Seg n holds
D1 . i is Subset of REAL

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

end;

then A19: CarProduct D1 is Subset of (CarProduct ((Seg n) --> REAL)) by FINSEQ_1:3, Th11;
then reconsider I1 = CarProduct D1 as Subset of (CarProduct ((Seg n) --> RNS_Real)) by MEASUR15:42;
reconsider f0 = f * (CarProd ((Seg (n + 1)) --> RNS_Real)) as PartFunc of [:(CarProduct ((Seg n) --> RNS_Real)),RNS_Real:],RNS_Real by MEASUR15:38;
A20: dom f0 = [:I1,Dk1:] by A15, A7, A1, Th4;
hence dom (ProjPMap1 (|.(R_EAL g0).|,x)) = D . (n + 1) by A19, A5, A6, A11, A7, A8, MESFUN16:27; :: thesis:
A21: f0 is_continuous_on dom f0 by A16, A15, MEASUR15:38;
then Pg is continuous by A5, A6, A11, A9, Th25;
hence Pg | Dk1 is continuous ; :: thesis:
thus ( Pg | Dk1 is bounded & Pg is_integrable_on Dk1 ) by A19, A5, A6, A11, A8, A20, A21, A9, Th28; :: thesis:
Pg is_integrable_on L-Meas by A19, A5, A6, A11, A20, A21, A9, Th31;
hence ProjPMap1 (|.(R_EAL g0).|,x) is_integrable_on L-Meas by A9, MESFUNC5:def 7; :: thesis:
thus ( Integral (L-Meas,(ProjPMap1 (|.(R_EAL g0).|,x))) = integral (Pg,Dk1) & (Integral2 (L-Meas,|.(R_EAL g0).|)) . x = integral (Pg,Dk1) ) by A19, A5, A6, A8, A9, A11, A20, A21, Th32; :: thesis: