let n be non zero Nat; :: thesis:
let D be n -element FinSequence; :: thesis:
let I be Subset of (CarProduct ((Seg n) --> RNS_Real)); :: thesis:
let J be closed_interval Subset of REAL; :: thesis:
let f be PartFunc of [:(CarProduct ((Seg n) --> RNS_Real)),RNS_Real:],RNS_Real; :: thesis:
let g be PartFunc of [:(CarProduct ((Seg n) --> REAL)),REAL:],REAL; :: thesis:
assume that
A1: for i being Nat st i in Seg n holds
D . i is closed_interval Subset of REAL and
A2: I = CarProduct D and
A3: [:I,J:] = dom f and
A4: f is_continuous_on [:I,J:] and
A5: f = g ; :: thesis:
A6: ex I1 being Subset of (CarProduct ((Seg n) --> RNS_Real)) st
( I1 = CarProduct D & I1 is compact )

proof

per cases ;

suppose D is non-empty ; :: thesis:

then reconsider D1 = D as non-empty n -element FinSequence ;
for i being Nat st i in Seg n holds
D1 . i is closed_interval Subset of REAL by A1;
hence ex I1 being Subset of (CarProduct ((Seg n) --> RNS_Real)) st
( I1 = CarProduct D & I1 is compact ) by MEASUR15:51; :: thesis:

end;

suppose A7: not D is non-empty ; :: thesis:

then A8: CarProduct D = {} by Th6;
CarProduct D c= the carrier of (CarProduct ((Seg n) --> RNS_Real)) by A7, Th6;
then reconsider I1 = CarProduct D as Subset of (CarProduct ((Seg n) --> RNS_Real)) ;
I1 is compact by A8;
hence ex I1 being Subset of (CarProduct ((Seg n) --> RNS_Real)) st
( I1 = CarProduct D & I1 is compact ) ; :: thesis:

end;

reconsider J1 = J as Subset of RNS_Real ;
A9: J1 is compact by MESFUN16:7;
reconsider E = [:(CarProduct D),J1:] as Subset of [:(CarProduct ((Seg n) --> RNS_Real)),RNS_Real:] by A6, A9, MESFUN16:8;
A10: for i being Nat st i in Seg n holds
D . i is Interval by A1;
then reconsider E = E as Element of sigma (measurable_rectangles ((Prod_Field (L-Field n)),L-Field)) by A2, Th49;
for i being Nat st i in Seg n holds
D . i is Subset of REAL by A1;
then A11: I is Subset of (CarProduct ((Seg n) --> REAL)) by A2, FINSEQ_1:3, Th11;
then A12: g is E -measurable by A2, A3, A4, A5, Th33;
set Rg = R_EAL g;
A13: dom g = dom (R_EAL g) by MESFUNC5:def 7;
then A14: dom |.(R_EAL g).| = [:I,J:] by A3, A5, MESFUNC1:def 10;
A15: for x being Element of CarProduct ((Seg n) --> REAL) st x in (CarProduct ((Seg n) --> REAL)) \ I holds
(Integral2 (L-Meas,|.(R_EAL g).|)) . x = 0

proof

let x be Element of CarProduct ((Seg n) --> REAL); :: thesis:
assume x in (CarProduct ((Seg n) --> REAL)) \ I ; :: thesis:
then not x in I by XBOOLE_0:def 5;
then dom (ProjPMap1 (|.(R_EAL g).|,x)) = {} by A3, A5, A11, MESFUN16:27;
then Integral (L-Meas,(ProjPMap1 (|.(R_EAL g).|,x))) = 0 by MESFUN16:1;
hence (Integral2 (L-Meas,|.(R_EAL g).|)) . x = 0 by MESFUN12:def 8; :: thesis:

end;

A16: for x being Element of CarProduct ((Seg n) --> REAL)
for y being Element of REAL st x in I & y in J holds
( (ProjPMap1 (|.(R_EAL g).|,x)) . y = |.(R_EAL g).| . (x,y) & |.(R_EAL g).| . (x,y) = |.(g . [x,y]).| & |.(R_EAL g).| . (x,y) = |.g.| . [x,y] )

proof

end;

A20: for x being Element of CarProduct ((Seg n) --> REAL) st x in I holds
0 <= (Integral2 (L-Meas,|.(R_EAL g).|)) . x

proof

let x be Element of CarProduct ((Seg n) --> REAL); :: thesis:
assume A21: x in I ; :: thesis:
reconsider CD = J as Element of L-Field by MEASUR10:5, MEASUR12:75;
reconsider Pg = ProjPMap1 (|.(R_EAL g).|,x) as PartFunc of REAL,REAL by MESFUN16:30;
A22: dom Pg = J by A21, A3, A11, A5, MESFUN16:27;
Pg is_integrable_on L-Meas by A3, A4, A5, A11, Th31;
then consider E being Element of L-Field such that
A23: ( E = dom (R_EAL Pg) & R_EAL Pg is E -measurable ) by MESFUNC5:def 17;
( E = dom Pg & R_EAL Pg is E -measurable ) by A23, MESFUNC5:def 7;
then A24: Pg is CD -measurable by A22;
R_EAL Pg = ProjPMap1 (|.(R_EAL g).|,x) by MESFUNC5:def 7;
then A25: (Integral2 (L-Meas,|.(R_EAL g).|)) . x = Integral (L-Meas,Pg) by MESFUN12:def 8;
for y being object st y in dom (Pg | J) holds
0 <= (Pg | J) . y

proof

end;

hence 0 <= (Integral2 (L-Meas,|.(R_EAL g).|)) . x by A22, A24, A25, MESFUNC6:52, MESFUNC6:84; :: thesis:

end;

proof

let r be Element of CarProduct ((Seg n) --> REAL); :: thesis:
( r in I or r in NI ) by A33, XBOOLE_0:def 3;
hence 0 <= (Integral2 (L-Meas,|.(R_EAL g).|)) . r by A20, A15; :: thesis:

end;

then A37: Integral2 (L-Meas,|.(R_EAL g).|) is nonnegative ;
for r being Real holds H /\ (less_dom ((Integral2 (L-Meas,|.(R_EAL g).|)),r)) in Prod_Field (L-Field n)

proof

per cases ;

suppose A39: r <= 0 ; :: thesis:

less_dom ((Integral2 (L-Meas,|.(R_EAL g).|)),r) = {}

proof

assume less_dom ((Integral2 (L-Meas,|.(R_EAL g).|)),r) <> {} ; :: thesis:
then consider x being object such that
A40: x in less_dom ((Integral2 (L-Meas,|.(R_EAL g).|)),r) by XBOOLE_0:def 1;
( x in dom (Integral2 (L-Meas,|.(R_EAL g).|)) & (Integral2 (L-Meas,|.(R_EAL g).|)) . x < r ) by MESFUNC1:def 11, A40;
hence contradiction by A36, A39; :: thesis:

end;

hence H /\ (less_dom ((Integral2 (L-Meas,|.(R_EAL g).|)),r)) in Prod_Field (L-Field n) by PROB_1:4; :: thesis:

end;

suppose A41: 0 < r ; :: thesis:

proof

let z be object ; :: thesis:

hereby :: thesis:

per cases by A42, A33, XBOOLE_0:def 3;

suppose A44: z in I ; :: thesis:

end;

suppose z in NI ; :: thesis:

hence z in (less_dom (((Integral2 (L-Meas,|.(R_EAL g).|)) | I),r)) \/ NI by XBOOLE_0:def 3; :: thesis:

end;

assume z in (less_dom (((Integral2 (L-Meas,|.(R_EAL g).|)) | I),r)) \/ NI ; :: thesis:

per cases by XBOOLE_0:def 3;

suppose A45: z in less_dom (((Integral2 (L-Meas,|.(R_EAL g).|)) | I),r) ; :: thesis:

end;

suppose A47: z in NI ; :: thesis:

then reconsider x = z as Element of CarProduct ((Seg n) --> REAL) ;
A48: (Integral2 (L-Meas,|.(R_EAL g).|)) . x < r by A41, A47, A15;
dom (Integral2 (L-Meas,|.(R_EAL g).|)) = CarProduct ((Seg n) --> REAL) by FUNCT_2:def 1;
hence z in less_dom ((Integral2 (L-Meas,|.(R_EAL g).|)),r) by A48, MESFUNC1:def 11; :: thesis:

end;

end;

proof

end;

then Integral ((Prod_Measure (L-Meas n)),((Integral2 (L-Meas,|.(R_EAL g).|)) | NI)) = 0 * ((Prod_Measure (L-Meas n)) . (dom ((Integral2 (L-Meas,|.(R_EAL g).|)) | NI))) by A27, A29, PROB_1:6, MEASUR10:27;
then Integral ((Prod_Measure (L-Meas n)),((Integral2 (L-Meas,|.(R_EAL g).|)) | I)) = Integral ((Prod_Measure (L-Meas n)),(Integral2 (L-Meas,|.(R_EAL g).|))) by A52, XXREAL_3:4;
then A55: R_EAL g is_integrable_on Prod_Measure ((Prod_Measure (L-Meas n)),L-Meas) by A12, A2, A3, A5, A13, A32, MESFUN16:5, A53, MESFUN13:11;
for x being Element of CarProduct ((Seg n) --> REAL) holds (Integral2 (L-Meas,|.(R_EAL g).|)) . x < +infty

proof

let x be Element of CarProduct ((Seg n) --> REAL); :: thesis:

per cases by A33, XBOOLE_0:def 3;

suppose A56: x in I ; :: thesis:

end;

suppose x in NI ; :: thesis:

hence (Integral2 (L-Meas,|.(R_EAL g).|)) . x < +infty by A15; :: thesis:

end;

hence ( g is_integrable_on Prod_Measure ((Prod_Measure (L-Meas n)),L-Meas) & ( for x being Element of CarProduct ((Seg n) --> REAL) holds (Integral2 (L-Meas,|.(R_EAL g).|)) . x < +infty ) & ( for U being Element of Prod_Field (L-Field n) holds Integral2 (L-Meas,(R_EAL g)) is U -measurable ) & Integral2 (L-Meas,(R_EAL g)) is_integrable_on Prod_Measure (L-Meas n) & Integral ((Prod_Measure ((Prod_Measure (L-Meas n)),L-Meas)),g) = Integral ((Prod_Measure (L-Meas n)),(Integral2 (L-Meas,(R_EAL g)))) ) by A53, A55, MESFUN16:5, MESFUN13:32; :: thesis: