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 ;
J1 is compact by MESFUN16:7;
then reconsider E = [:(CarProduct D),J1:] as Subset of [:(CarProduct ((Seg n) --> RNS_Real)),RNS_Real:] by A6, MESFUN16:8;
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 A9: I is Subset of (CarProduct ((Seg n) --> REAL)) by A2, FINSEQ_1:3, Th11;
then A10: g is E -measurable by A2, A3, A4, A5, Th33;
set Rg = R_EAL g;
dom g = dom (R_EAL g) by MESFUNC5:def 7;
then A11: dom |.(R_EAL g).| = [:I,J:] by A3, A5, MESFUNC1:def 10;
A12: for y being Element of REAL st y in REAL \ J holds
(Integral1 ((Prod_Measure (L-Meas n)),|.(R_EAL g).|)) . y = 0

proof

let y be Element of REAL ; :: thesis:
assume y in REAL \ J ; :: thesis:
then not y in J by XBOOLE_0:def 5;
then A13: dom (ProjPMap2 (|.(R_EAL g).|,y)) = {} by A3, A5, A9, MESFUN16:28;
(Integral1 ((Prod_Measure (L-Meas n)),|.(R_EAL g).|)) . y = Integral ((Prod_Measure (L-Meas n)),(ProjPMap2 (|.(R_EAL g).|,y))) by MESFUN12:def 7;
hence (Integral1 ((Prod_Measure (L-Meas n)),|.(R_EAL g).|)) . y = 0 by A13, MESFUN16:1; :: thesis:

end;

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

proof

end;

A19: for y being Element of REAL st y in J holds
0 <= (Integral1 ((Prod_Measure (L-Meas n)),|.(R_EAL g).|)) . y

proof

let y be Element of REAL ; :: thesis:
assume A20: y in J ; :: thesis:
for i being Nat st i in Seg n holds
D . i is Interval by A1;
then reconsider AB = I as Element of Prod_Field (L-Field n) by A2, Th9;
reconsider Pg = ProjPMap2 (|.(R_EAL g).|,y) as PartFunc of (CarProduct ((Seg n) --> REAL)),REAL by MESFUN16:30;
A21: ProjPMap2 (|.(R_EAL g).|,y) = R_EAL Pg by MESFUNC5:def 7;
A22: dom Pg = I by A20, A3, A9, A5, MESFUN16:28;
A23: Pg is AB -measurable by A21, A1, A20, A3, A2, A4, A5, Th47;
A24: Integral ((Prod_Measure (L-Meas n)),Pg) = (Integral1 ((Prod_Measure (L-Meas n)),|.(R_EAL g).|)) . y by A1, A20, A2, A3, A4, A5, A21, Th48;
for x being object st x in dom (Pg | I) holds
0 <= (Pg | I) . x

proof

end;

hence 0 <= (Integral1 ((Prod_Measure (L-Meas n)),|.(R_EAL g).|)) . y by A22, A23, A24, MESFUNC6:52, MESFUNC6:84; :: thesis:

end;

proof

per cases ;

suppose not J is empty ; :: thesis:

then reconsider J1 = J as non empty closed_interval Subset of REAL ;
( S || J1 is bounded & S is_integrable_on J1 ) by A28, A1, A2, A3, A4, A5, Th53, INTEGRA5:10, INTEGRA5:11;
hence S is_integrable_on L-Meas by A26, A28, MESFUN14:49; :: thesis:

end;

suppose A29: J is empty ; :: thesis:

reconsider E = {} as Element of L-Field by MEASURE1:7;
A30: E = dom (R_EAL S) by A28, A29, MESFUNC5:def 7;
for x being Element of REAL st x in dom (R_EAL S) holds
(R_EAL S) . x = 0 by A28, A29, MESFUNC5:def 7;
hence S is_integrable_on L-Meas by A30, LPSPACE1:22; :: thesis:

end;

then A31: T0 is_integrable_on L-Meas by MESFUNC5:def 7;
then A32: Integral (L-Meas,T0) < +infty by MESFUNC5:96;
A33: H \ J is Element of L-Field by A26, PROB_1:6;
A34: J \/ (H \ J) = REAL by XBOOLE_1:45;
then A35: (Integral1 ((Prod_Measure (L-Meas n)),|.(R_EAL g).|)) | (J \/ (H \ J)) = Integral1 ((Prod_Measure (L-Meas n)),|.(R_EAL g).|) ;
A36: J /\ (H \ J) = {} by XBOOLE_1:85, XBOOLE_0:def 7;
A37: for r being Element of REAL holds 0 <= (Integral1 ((Prod_Measure (L-Meas n)),|.(R_EAL g).|)) . r

proof

let r be Element of REAL ; :: thesis:
( r in J or r in H \ J ) by A34, XBOOLE_0:def 3;
hence 0 <= (Integral1 ((Prod_Measure (L-Meas n)),|.(R_EAL g).|)) . r by A19, A12; :: thesis:

end;

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

proof

let r be Real; :: thesis:
consider H0 being Element of L-Field such that
A39: ( H0 = dom T0 & T0 is H0 -measurable ) by A31, MESFUNC5:def 17;

per cases ;

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

less_dom ((Integral1 ((Prod_Measure (L-Meas n)),|.(R_EAL g).|)),r) = {}

proof

assume less_dom ((Integral1 ((Prod_Measure (L-Meas n)),|.(R_EAL g).|)),r) <> {} ; :: thesis:
then consider y being object such that
A41: y in less_dom ((Integral1 ((Prod_Measure (L-Meas n)),|.(R_EAL g).|)),r) by XBOOLE_0:def 1;
( y in dom (Integral1 ((Prod_Measure (L-Meas n)),|.(R_EAL g).|)) & (Integral1 ((Prod_Measure (L-Meas n)),|.(R_EAL g).|)) . y < r ) by MESFUNC1:def 11, A41;
hence contradiction by A37, A40; :: thesis:

end;

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

end;

suppose A42: 0 < r ; :: thesis:

for z being object holds
( z in less_dom ((Integral1 ((Prod_Measure (L-Meas n)),|.(R_EAL g).|)),r) iff z in (less_dom (T0,r)) \/ (H \ J) )

proof

let z be object ; :: thesis:

hereby :: thesis:

assume A43: z in less_dom ((Integral1 ((Prod_Measure (L-Meas n)),|.(R_EAL g).|)),r) ; :: thesis:
then A44: ( z in dom (Integral1 ((Prod_Measure (L-Meas n)),|.(R_EAL g).|)) & (Integral1 ((Prod_Measure (L-Meas n)),|.(R_EAL g).|)) . z < r ) by MESFUNC1:def 11;
reconsider y = z as Element of REAL by A43;

per cases by A43, A34, XBOOLE_0:def 3;

suppose A45: z in J ; :: thesis:

then T0 . z < r by FUNCT_1:49, A44;
then z in less_dom (T0,r) by A45, A28, MESFUNC1:def 11;
hence z in (less_dom (T0,r)) \/ (H \ J) by XBOOLE_0:def 3; :: thesis:

end;

suppose z in H \ J ; :: thesis:

hence z in (less_dom (T0,r)) \/ (H \ J) by XBOOLE_0:def 3; :: thesis:

end;

assume z in (less_dom (T0,r)) \/ (H \ J) ; :: thesis:

per cases by XBOOLE_0:def 3;

suppose A46: z in less_dom (T0,r) ; :: thesis:

then ( z in dom T0 & T0 . z < r ) by MESFUNC1:def 11;
then A47: (Integral1 ((Prod_Measure (L-Meas n)),|.(R_EAL g).|)) . z < r by A28, FUNCT_1:49;
dom (Integral1 ((Prod_Measure (L-Meas n)),|.(R_EAL g).|)) = REAL by FUNCT_2:def 1;
hence z in less_dom ((Integral1 ((Prod_Measure (L-Meas n)),|.(R_EAL g).|)),r) by A46, A47, MESFUNC1:def 11; :: thesis:

end;

suppose A48: z in H \ J ; :: thesis:

then reconsider y = z as Element of REAL ;
A49: (Integral1 ((Prod_Measure (L-Meas n)),|.(R_EAL g).|)) . y < r by A42, A48, A12;
dom (Integral1 ((Prod_Measure (L-Meas n)),|.(R_EAL g).|)) = REAL by FUNCT_2:def 1;
hence z in less_dom ((Integral1 ((Prod_Measure (L-Meas n)),|.(R_EAL g).|)),r) by A49, MESFUNC1:def 11; :: thesis:

end;

then less_dom ((Integral1 ((Prod_Measure (L-Meas n)),|.(R_EAL g).|)),r) = (less_dom (T0,r)) \/ (H \ J) by TARSKI:2;
then A50: H /\ (less_dom ((Integral1 ((Prod_Measure (L-Meas n)),|.(R_EAL g).|)),r)) = (J /\ ((less_dom (T0,r)) \/ (H \ J))) \/ ((H \ J) /\ ((less_dom (T0,r)) \/ (H \ J))) by A34, XBOOLE_1:23;
J /\ ((less_dom (T0,r)) \/ (H \ J)) = (J /\ (less_dom (T0,r))) \/ {} by A36, XBOOLE_1:23;
then A51: J /\ ((less_dom (T0,r)) \/ (H \ J)) in L-Field by A27, A39;
A52: less_dom (T0,r) c= J by A28, MESFUNC1:def 11;
(H \ J) /\ ((less_dom (T0,r)) \/ (H \ J)) = ((H \ J) /\ (less_dom (T0,r))) \/ ((H \ J) /\ (H \ J)) by XBOOLE_1:23;
then (H \ J) /\ ((less_dom (T0,r)) \/ (H \ J)) = {} \/ ((H \ J) /\ (H \ J)) by A52;
hence H /\ (less_dom ((Integral1 ((Prod_Measure (L-Meas n)),|.(R_EAL g).|)),r)) in L-Field by A33, A50, A51, PROB_1:3; :: thesis:

end;

then Integral1 ((Prod_Measure (L-Meas n)),|.(R_EAL g).|) is H -measurable ;
then A53: Integral (L-Meas,(Integral1 ((Prod_Measure (L-Meas n)),|.(R_EAL g).|))) = (Integral (L-Meas,T0)) + (Integral (L-Meas,T1)) by A27, A26, A33, A35, A38, MESFUNC5:91, XBOOLE_1:79;
A54: Prod_Measure (L-Meas n) is sigma_finite by MEASUR15:36;
A55: E = dom (R_EAL g) by A2, A3, A5, MESFUNC5:def 7;
for y being object st y in dom T1 holds
T1 . y = 0

proof

let y be object ; :: thesis:
assume A56: y in dom T1 ; :: thesis:
then reconsider r = y as Element of REAL ;
A57: ( y in dom (Integral1 ((Prod_Measure (L-Meas n)),|.(R_EAL g).|)) & y in H \ J ) by A56, RELAT_1:57;
(Integral1 ((Prod_Measure (L-Meas n)),|.(R_EAL g).|)) . r = 0 by A56, A12, RELAT_1:57;
hence T1 . y = 0 by A57, FUNCT_1:49; :: thesis:

end;

then Integral (L-Meas,T1) = 0 * (L-Meas . (dom T1)) by A27, A26, PROB_1:6, MEASUR10:27;
then Integral (L-Meas,T0) = Integral (L-Meas,(Integral1 ((Prod_Measure (L-Meas n)),|.(R_EAL g).|))) by A53, XXREAL_3:4;
then A58: R_EAL g is_integrable_on Prod_Measure ((Prod_Measure (L-Meas n)),L-Meas) by A32, A54, A55, MESFUN13:10, A10, MESFUN16:5;
for y being Element of REAL holds (Integral1 ((Prod_Measure (L-Meas n)),|.(R_EAL g).|)) . y < +infty

proof

let y be Element of REAL ; :: thesis:

per cases by A34, XBOOLE_0:def 3;

suppose A59: y in J ; :: thesis:

end;

suppose y in H \ J ; :: thesis:

hence (Integral1 ((Prod_Measure (L-Meas n)),|.(R_EAL g).|)) . y < +infty by A12; :: thesis:

end;

hence ( g is_integrable_on Prod_Measure ((Prod_Measure (L-Meas n)),L-Meas) & ( for y being Element of REAL holds (Integral1 ((Prod_Measure (L-Meas n)),|.(R_EAL g).|)) . y < +infty ) & ( for V being Element of L-Field holds Integral1 ((Prod_Measure (L-Meas n)),(R_EAL g)) is V -measurable ) & Integral1 ((Prod_Measure (L-Meas n)),(R_EAL g)) is_integrable_on L-Meas & Integral ((Prod_Measure ((Prod_Measure (L-Meas n)),L-Meas)),g) = Integral (L-Meas,(Integral1 ((Prod_Measure (L-Meas n)),(R_EAL g)))) ) by A54, A58, MESFUN16:5, MESFUN13:33; :: thesis: