let n be non zero Nat; :: thesis: for D being n -element FinSequence
for f being PartFunc of (REAL-NS n),RNS_Real
for g being PartFunc of (REAL n),REAL
for G being PartFunc of (CarProduct ((Seg n) --> REAL)),REAL st ( for i being Nat st i in Seg n holds
D . i is closed_interval Subset of REAL ) & f is_continuous_on product D & dom f = product D & g = f & G = f * (CarProd ((Seg n) --> REAL)) holds
( G is_integrable_on Prod_Measure (L-Meas n) & g is_integrable_on XL-Meas n & Integral ((XL-Meas n),g) = Integral ((Prod_Measure (L-Meas n)),G) )
let D be n -element FinSequence; :: thesis: for f being PartFunc of (REAL-NS n),RNS_Real
for g being PartFunc of (REAL n),REAL
for G being PartFunc of (CarProduct ((Seg n) --> REAL)),REAL st ( for i being Nat st i in Seg n holds
D . i is closed_interval Subset of REAL ) & f is_continuous_on product D & dom f = product D & g = f & G = f * (CarProd ((Seg n) --> REAL)) holds
( G is_integrable_on Prod_Measure (L-Meas n) & g is_integrable_on XL-Meas n & Integral ((XL-Meas n),g) = Integral ((Prod_Measure (L-Meas n)),G) )
let f be PartFunc of (REAL-NS n),RNS_Real; :: thesis: for g being PartFunc of (REAL n),REAL
for G being PartFunc of (CarProduct ((Seg n) --> REAL)),REAL st ( for i being Nat st i in Seg n holds
D . i is closed_interval Subset of REAL ) & f is_continuous_on product D & dom f = product D & g = f & G = f * (CarProd ((Seg n) --> REAL)) holds
( G is_integrable_on Prod_Measure (L-Meas n) & g is_integrable_on XL-Meas n & Integral ((XL-Meas n),g) = Integral ((Prod_Measure (L-Meas n)),G) )
let g be PartFunc of (REAL n),REAL; :: thesis: for G being PartFunc of (CarProduct ((Seg n) --> REAL)),REAL st ( for i being Nat st i in Seg n holds
D . i is closed_interval Subset of REAL ) & f is_continuous_on product D & dom f = product D & g = f & G = f * (CarProd ((Seg n) --> REAL)) holds
( G is_integrable_on Prod_Measure (L-Meas n) & g is_integrable_on XL-Meas n & Integral ((XL-Meas n),g) = Integral ((Prod_Measure (L-Meas n)),G) )
let G be PartFunc of (CarProduct ((Seg n) --> REAL)),REAL; :: thesis: ( ( for i being Nat st i in Seg n holds
D . i is closed_interval Subset of REAL ) & f is_continuous_on product D & dom f = product D & g = f & G = f * (CarProd ((Seg n) --> REAL)) implies ( G is_integrable_on Prod_Measure (L-Meas n) & g is_integrable_on XL-Meas n & Integral ((XL-Meas n),g) = Integral ((Prod_Measure (L-Meas n)),G) ) )
assume that
A1: for i being Nat st i in Seg n 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 and
A5: G = f * (CarProd ((Seg n) --> REAL)) ; :: thesis: ( G is_integrable_on Prod_Measure (L-Meas n) & g is_integrable_on XL-Meas n & Integral ((XL-Meas n),g) = Integral ((Prod_Measure (L-Meas n)),G) )
set I = CarProd ((Seg n) --> RNS_Real);
consider CX being non-empty n -element FinSequence such that
A6: ( CX = carr ((Seg n) --> RNS_Real) & CarProduct CX = the carrier of (CarProduct ((Seg n) --> RNS_Real)) & CarProd ((Seg n) --> RNS_Real) = CarProd CX & CarProd ((Seg n) --> RNS_Real) is bijective ) by MEASUR15:def 7;
A7: REAL-NS n = product ((Seg n) --> RNS_Real) by Th61;
then A8: the carrier of (REAL-NS n) = REAL n by Th61;
then A9: rng (CarProd ((Seg n) --> RNS_Real)) = REAL n by A6, A7, FUNCT_2:def 3;
A10: dom (CarProd ((Seg n) --> RNS_Real)) = the carrier of (CarProduct ((Seg n) --> RNS_Real)) by FUNCT_2:def 1;
then ( dom ((CarProd ((Seg n) --> RNS_Real)) ") = REAL n & rng ((CarProd ((Seg n) --> RNS_Real)) ") = the carrier of (CarProduct ((Seg n) --> RNS_Real)) ) by A6, A9, FUNCT_1:33;
then reconsider J = (CarProd ((Seg n) --> RNS_Real)) " as Function of (REAL n), the carrier of (CarProduct ((Seg n) --> RNS_Real)) by FUNCT_2:1;
reconsider H = (R_EAL G) * J as PartFunc of (REAL n),ExtREAL ;
A11: CarProd ((Seg n) --> RNS_Real) = CarProd ((Seg n) --> REAL) by MEASUR15:70;
H = G * J by MESFUNC5:def 7;
then H = f * ((CarProd ((Seg n) --> RNS_Real)) * ((CarProd ((Seg n) --> RNS_Real)) ")) by A5, A11, RELAT_1:36;
then H = f * (id (rng (CarProd ((Seg n) --> RNS_Real)))) by A6, FUNCT_1:39;
then A12: H = f by A8, A9, FUNCT_2:17;
reconsider F = f * (CarProd ((Seg n) --> RNS_Real)) as PartFunc of (CarProduct ((Seg n) --> RNS_Real)),RNS_Real ;
for i being Nat st i in Seg n holds
D . i is Subset of REAL by A1;
then A13: F is_continuous_on CarProduct D by A2, A3, Th62;
A14: for i being Nat st i in Seg n holds
D . i c= REAL

proof

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

end;

CarProduct D c= CarProduct ((Seg n) --> REAL)

proof

per cases ( D is non-empty or not D is non-empty ) ;

suppose D is non-empty ; :: thesis: CarProduct D c= CarProduct ((Seg n) --> REAL)

then reconsider D1 = D as non-empty n -element FinSequence ;
CarProduct D1 c= CarProduct ((Seg n) --> REAL) by A14, MEASUR15:34;
hence CarProduct D c= CarProduct ((Seg n) --> REAL) ; :: thesis: verum

end;

suppose not D is non-empty ; :: thesis: CarProduct D c= CarProduct ((Seg n) --> REAL)

hence CarProduct D c= CarProduct ((Seg n) --> REAL) by Th6; :: thesis: verum

end;

end;

end;

then A15: CarProduct D c= dom (CarProd ((Seg n) --> RNS_Real)) by A10, MEASUR15:42;
A16: product D = (CarProd ((Seg n) --> RNS_Real)) .: (CarProduct D) by A14, A11, Th12;
dom F = (CarProd ((Seg n) --> RNS_Real)) " (dom f) by RELAT_1:147;
hence A17: G is_integrable_on Prod_Measure (L-Meas n) by A1, A3, A5, A6, A11, A16, A15, A13, Th43, FUNCT_1:94; :: thesis: ( g is_integrable_on XL-Meas n & Integral ((XL-Meas n),g) = Integral ((Prod_Measure (L-Meas n)),G) )
then H is_integrable_on XL-Meas n by A11, MEASUR14:55;
hence g is_integrable_on XL-Meas n by A4, A12, MESFUNC5:def 7; :: thesis: Integral ((XL-Meas n),g) = Integral ((Prod_Measure (L-Meas n)),G)
ex A being Element of Prod_Field (L-Field n) st
( A = dom (R_EAL G) & R_EAL G is A -measurable ) by A17, MESFUNC5:def 17;
hence Integral ((XL-Meas n),g) = Integral ((Prod_Measure (L-Meas n)),G) by A4, A12, A11, MESFUNC5:def 7, MEASUR14:54; :: thesis: verum