let n be non zero Nat; :: thesis: for D being n -element FinSequence
for I being Subset of (CarProduct ((Seg n) --> RNS_Real))
for J being non empty closed_interval Subset of REAL
for f being PartFunc of [:(CarProduct ((Seg n) --> RNS_Real)),RNS_Real:],RNS_Real
for g being PartFunc of [:(CarProduct ((Seg n) --> REAL)),REAL:],REAL
for G1 being PartFunc of REAL,REAL st ( for i being Nat st i in Seg n holds
D . i is closed_interval Subset of REAL ) & I = CarProduct D & [:I,J:] = dom f & f is_continuous_on [:I,J:] & f = g & G1 = (Integral1 ((Prod_Measure (L-Meas n)),(R_EAL g))) | J holds
Integral ((Prod_Measure ((Prod_Measure (L-Meas n)),L-Meas)),(R_EAL g)) = integral (G1,J)
let D be n -element FinSequence; :: thesis: for I being Subset of (CarProduct ((Seg n) --> RNS_Real))
for J being non empty closed_interval Subset of REAL
for f being PartFunc of [:(CarProduct ((Seg n) --> RNS_Real)),RNS_Real:],RNS_Real
for g being PartFunc of [:(CarProduct ((Seg n) --> REAL)),REAL:],REAL
for G1 being PartFunc of REAL,REAL st ( for i being Nat st i in Seg n holds
D . i is closed_interval Subset of REAL ) & I = CarProduct D & [:I,J:] = dom f & f is_continuous_on [:I,J:] & f = g & G1 = (Integral1 ((Prod_Measure (L-Meas n)),(R_EAL g))) | J holds
Integral ((Prod_Measure ((Prod_Measure (L-Meas n)),L-Meas)),(R_EAL g)) = integral (G1,J)
let I be Subset of (CarProduct ((Seg n) --> RNS_Real)); :: thesis: for J being non empty closed_interval Subset of REAL
for f being PartFunc of [:(CarProduct ((Seg n) --> RNS_Real)),RNS_Real:],RNS_Real
for g being PartFunc of [:(CarProduct ((Seg n) --> REAL)),REAL:],REAL
for G1 being PartFunc of REAL,REAL st ( for i being Nat st i in Seg n holds
D . i is closed_interval Subset of REAL ) & I = CarProduct D & [:I,J:] = dom f & f is_continuous_on [:I,J:] & f = g & G1 = (Integral1 ((Prod_Measure (L-Meas n)),(R_EAL g))) | J holds
Integral ((Prod_Measure ((Prod_Measure (L-Meas n)),L-Meas)),(R_EAL g)) = integral (G1,J)
let J be non empty closed_interval Subset of REAL; :: thesis: for f being PartFunc of [:(CarProduct ((Seg n) --> RNS_Real)),RNS_Real:],RNS_Real
for g being PartFunc of [:(CarProduct ((Seg n) --> REAL)),REAL:],REAL
for G1 being PartFunc of REAL,REAL st ( for i being Nat st i in Seg n holds
D . i is closed_interval Subset of REAL ) & I = CarProduct D & [:I,J:] = dom f & f is_continuous_on [:I,J:] & f = g & G1 = (Integral1 ((Prod_Measure (L-Meas n)),(R_EAL g))) | J holds
Integral ((Prod_Measure ((Prod_Measure (L-Meas n)),L-Meas)),(R_EAL g)) = integral (G1,J)
let f be PartFunc of [:(CarProduct ((Seg n) --> RNS_Real)),RNS_Real:],RNS_Real; :: thesis: for g being PartFunc of [:(CarProduct ((Seg n) --> REAL)),REAL:],REAL
for G1 being PartFunc of REAL,REAL st ( for i being Nat st i in Seg n holds
D . i is closed_interval Subset of REAL ) & I = CarProduct D & [:I,J:] = dom f & f is_continuous_on [:I,J:] & f = g & G1 = (Integral1 ((Prod_Measure (L-Meas n)),(R_EAL g))) | J holds
Integral ((Prod_Measure ((Prod_Measure (L-Meas n)),L-Meas)),(R_EAL g)) = integral (G1,J)
let g be PartFunc of [:(CarProduct ((Seg n) --> REAL)),REAL:],REAL; :: thesis: for G1 being PartFunc of REAL,REAL st ( for i being Nat st i in Seg n holds
D . i is closed_interval Subset of REAL ) & I = CarProduct D & [:I,J:] = dom f & f is_continuous_on [:I,J:] & f = g & G1 = (Integral1 ((Prod_Measure (L-Meas n)),(R_EAL g))) | J holds
Integral ((Prod_Measure ((Prod_Measure (L-Meas n)),L-Meas)),(R_EAL g)) = integral (G1,J)
let G1 be PartFunc of REAL,REAL; :: thesis: ( ( for i being Nat st i in Seg n holds
D . i is closed_interval Subset of REAL ) & I = CarProduct D & [:I,J:] = dom f & f is_continuous_on [:I,J:] & f = g & G1 = (Integral1 ((Prod_Measure (L-Meas n)),(R_EAL g))) | J implies Integral ((Prod_Measure ((Prod_Measure (L-Meas n)),L-Meas)),(R_EAL g)) = integral (G1,J) )
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 and
A6: G1 = (Integral1 ((Prod_Measure (L-Meas n)),(R_EAL g))) | J ; :: thesis: Integral ((Prod_Measure ((Prod_Measure (L-Meas n)),L-Meas)),(R_EAL g)) = integral (G1,J)
set Rg = R_EAL g;
set NJ = REAL \ J;
set RG1 = Integral1 ((Prod_Measure (L-Meas n)),(R_EAL g));
reconsider F0 = (Integral1 ((Prod_Measure (L-Meas n)),(R_EAL g))) | J, F1 = (Integral1 ((Prod_Measure (L-Meas n)),(R_EAL g))) | (REAL \ J) as PartFunc of REAL,ExtREAL by PARTFUN1:11;
A7: dom (Integral1 ((Prod_Measure (L-Meas n)),(R_EAL g))) = REAL by FUNCT_2:def 1;
A8: dom ((Integral1 ((Prod_Measure (L-Meas n)),(R_EAL g))) | J) = J by FUNCT_2:def 1;
A9: J is Element of L-Field by MEASUR10:5, MEASUR12:75;
( G1 | J is bounded & G1 is_integrable_on J ) by A8, A1, A2, A3, A4, A5, A6, Th54, INTEGRA5:10, INTEGRA5:11;
then A10: Integral (L-Meas,(G1 | J)) = integral (G1,J) by A6, A9, A8, MESFUN14:49;
REAL in L-Field by PROB_1:5;
then A11: REAL \ J is Element of L-Field by A9, PROB_1:6;
A12: Integral ((Prod_Measure ((Prod_Measure (L-Meas n)),L-Meas)),g) = Integral (L-Meas,(Integral1 ((Prod_Measure (L-Meas n)),(R_EAL g)))) by A1, A2, A4, A3, A5, Lm4;
J \/ (REAL \ J) = REAL by XBOOLE_1:45;
then A13: (Integral1 ((Prod_Measure (L-Meas n)),(R_EAL g))) | (J \/ (REAL \ J)) = Integral1 ((Prod_Measure (L-Meas n)),(R_EAL g)) ;
Integral1 ((Prod_Measure (L-Meas n)),(R_EAL g)) is_integrable_on L-Meas by A1, A2, A4, A3, A5, Lm4;
then A14: Integral (L-Meas,(Integral1 ((Prod_Measure (L-Meas n)),(R_EAL g)))) = (Integral (L-Meas,F0)) + (Integral (L-Meas,F1)) by A9, A11, A13, XBOOLE_1:85, MESFUNC5:98;
for i being Nat st i in Seg n holds
D . i is Subset of REAL by A1;
then A15: CarProduct D is Subset of (CarProduct ((Seg n) --> REAL)) by FINSEQ_1:3, Th11;
for y being Element of REAL st y in dom F1 holds
F1 . y = 0

proof

let y be Element of REAL ; :: thesis: ( y in dom F1 implies F1 . y = 0 )
assume A16: y in dom F1 ; :: thesis: F1 . y = 0
then not y in J by A7, XBOOLE_0:def 5;
then A17: dom (ProjPMap2 ((R_EAL g),y)) = {} by A15, A2, A3, A5, 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;
then (Integral1 ((Prod_Measure (L-Meas n)),(R_EAL g))) . y = 0 by A17, MESFUN16:1;
hence F1 . y = 0 by A7, A16, FUNCT_1:49; :: thesis: verum

end;

then Integral (L-Meas,F1) = 0 by A11, A7, MESFUN12:57;
then Integral ((Prod_Measure ((Prod_Measure (L-Meas n)),L-Meas)),(R_EAL g)) = Integral (L-Meas,F0) by A12, A14, XXREAL_3:4;
hence Integral ((Prod_Measure ((Prod_Measure (L-Meas n)),L-Meas)),(R_EAL g)) = integral (G1,J) by A6, A10, MESFUNC5:def 7; :: thesis: verum